Commit 913c4922 authored by jfschaefer's avatar jfschaefer

some more useful comments

parent cbc68180
namespace http://mathhub.info/lbs1920/plnq ❚
// Names of relevant symbols:
delimiters:
OD, DD, MD
logical connectives:
wedge : ∧, neg : ¬, vee : ∨, Rightarrow : ⇒, Leftrightarrow : ⇔
other:
raa : ⟶, : ⊢
// Theory for predicate logic without quantifiers (PLNQ) ❚
theory PLNQ : ur:?LF =
// A type for propositions ❙
prop : type ❙
// Conjunction (AND) is a function that takes two propositions and creates a new one ❙
// We introduce a notation for it: The wedge (∧) ❙
// We also set a precedence to make it bind e.g. weaker than negation ❙
......@@ -27,7 +37,11 @@ theory PLNQ : ur:?LF =
// ⊢ (A ∧ B) is the type of proofs for A ∧ B ❙
andEliminationRight : {A, B} ⊢ (A ∧ B) ⟶ ⊢ A ❘ # andEr 3 ❙
implicationIntroduction : {A,B} (⊢ A ⟶ ⊢ B) ⟶ ⊢ (A ⇒ B) ❘ # implI 3 ❙
// TODO: ADD MISSING PROOF RULES... ❙
// Proof that A ∧ B ⇒ B ∧ A given any A and B ❙
andCommutativity : {A, B} ⊢ (A ∧ B ⇒ B ∧ A) ❘ =
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment