14 lines
585 B
Plaintext
14 lines
585 B
Plaintext
|
# Proof system for FOL
|
||
|
|
Axiom Group1 : substitution in propositional tautologies
|
||
|
|
Axiom Group2 : (\forall x \alpha -> \alpha[t,x]) for any term t substituting x in valid way (that is no free variable becomes bound).
|
||
|
|
Axiom Group3 : (\forall x (\alpha -> \beta) -> (\forall x \alpha -> \forall x \beta))
|
||
|
|
Axiom Group4 : (\alpha -> (\forall x \alpha)), when x is not a free variable in \alpha
|
||
|
|
|
||
|
|
## Then Axioms=I({Axiom group1, Axiom group2, Axiom group3, Axiom group4}, {\forall x, \forall y,...})
|
||
|
|
|
||
|
|
## Any formula has a proof if it belongs to I(Axioms,{MP}).
|
||
|
|
|
||
|
|
-- example of a proof.
|
||
|
|
|
||
|
|
|