¬A | 'not A'
A → B | 'if A, then B', 'A implies B' (the A is called the 'antecedent', and the B is called the 'consequent')
A & B | 'A and B'
A ∨ B | 'A or B or both'
A ⊻ B | 'A or B, but not both'
A ↔︎ B | 'A and B imply each other'
A ∧ B ∧ C | 'A, B, and C'
A ⋎ B ⋎ C | 'A or B or C, or any combination of them'
A ⩒ B ⩒ C | 'only one of A, B, and C is true'
A(x) | wff A containing x
A[x/y] | 'wff A, in which every instance of y has been substituted by x'
(∀x)A(x) | 'wff A obtains for all individual object substituting all occurrences of x in A', 'for all x, A is true'
(∃x)A(x) | 'wff A obtains for at least one individual object substituting all occurrences of x in A', 'there is something such that A is true'
(Ⅎx)A | 'every occurrence of x in wff A is bounded by a quantifier' (the Ⅎ can be read as 'unfree')
{a, b, c, ...} | 'the set containing a, b, c, ...'
x ∈ y | 'x is a member of y'
x ⊆ y | 'x is either a subset of y or identical to y'
x ⊂ y | 'x is a subset of y'
{x | P} | 'the set of all object that satisfies property P'
x = y | 'x is identical/equal to y'
There are two types of axioms and theorems:
Tautologies
Example: ⊢ (A ∨ ¬A)
Since 'A' can be any wff of L1+ZF, '[(A & B) ∨ ¬(A & B)]' is also an instance of the theorem '(A ∨ ¬A)', and thus also a tautology.
Inference rules
Example: ⊢A , ⊢(A → B) ⇒ ⊢B
The formulas before the '⇒', separated by the comma, are the hypotheses of the inference rule.
A proof of a theorem is as followed:
Line# Proof body (Justification)
Line# Proof body (Justification)
Line# Proof body (Justification)
...
Line# Proof body (Justification) QED
If an axiom/theorem is a tautology, then it can be inserted as a line at any point in the proof. The Justification for the Line would just its axiom/theorem #.
If an axiom/theorem is an inference rule, then its usage in a proof requires that the one or more hypothesis of that Rule is/are already present as a line(s) previously in the proof. The usage involves inserting a new line from the Rule being used, specifically the one that comes after the '⇒'. The justification for that Line would be the line# of each line cited as the hypothesis of the Rule, followed by the axiom/theorem#.
The usage of Axiom 22 'Deduction' is different in that it allows a hypothesis wff to be introduced directly into the proof and ends with deriving a conditional with that hypothesis as the antecedent:
Example:
1. 𝜑 (Justification)
...
4. 𝜓 (Justification)
5. H (hypothesis for Conditional Proof)
...
8. C (Justification)
9. H → C (5 - 8, Deduction ax. 22)