Why Are Axiom Schemas Important in Propositional Logic?

AI Thread Summary
Axiom schemas in propositional logic are essential as they allow for the formulation of infinitely many axioms, which represent valid logical structures. In predicate calculus, axioms are defined as well-formed formulas (wffs) that adhere to these schemas, ensuring that the derived theorems correspond to logically valid formulas or tautologies. The choice of axioms in propositional calculus is critical, as they must guarantee that the theorems are exactly the tautologies. Modus ponens is utilized with these axiom schemas to derive theorems by applying established instances of the schemas to reach conclusions. Overall, the structured use of axiom schemas facilitates rigorous theorem proving in logic.
Cinitiator
Messages
66
Reaction score
0
Actually, I have several questions:
1) Why are axiom schemas the way they are? What do they represent? I know that infinitely many axioms can be written using the axiom schema form. However, what's the formal definition of axioms in predicate calculus? I've heard that the formal definition of axioms is any wff which has the axiom schema form. If that's the case, what's so special about some wffs which can have infinitely many forms? Do they have any distinctive properties at all?

2) Why and how are they used for proving theorems / making other inferences?

3) How is modus ponens used with such axiom schemas to prove theorems?
 
Physics news on Phys.org
Cinitiator said:
Actually, I have several questions:
1) Why are axiom schemas the way they are? What do they represent? I know that infinitely many axioms can be written using the axiom schema form. However, what's the formal definition of axioms in predicate calculus? I've heard that the formal definition of axioms is any wff which has the axiom schema form. If that's the case, what's so special about some wffs which can have infinitely many forms? Do they have any distinctive properties at all?

2) Why and how are they used for proving theorems / making other inferences?

3) How is modus ponens used with such axiom schemas to prove theorems?

1)-2) Axioms can be different in different formal theories. But in all theories, the axioms of predicate calculus must be chosen so that the set of theorems (which can be derived from the axioms by the rules) is the same as the set of logically valid formulas. It we restrict ourselves to propositional calculus, logically valid formula is the same as tautology, so the axioms of propositional calculus are chosen so that the theorems are exactly the tautologies.

3) For example, suppose we have the following axiom schemas (among others):

A1. P->(Q->P).
A2. (P->(Q->R))->((P->Q)->(P->R)).

Then, let us derive the theorem P->P:

1. (P->((P->P)->P))->((P->(P->P))->(P->P)). Instances of A2.
2. P->((P->P)->P). Instances of A1.
3. (P->(P->P))->(P->P). MP: 1,2.
4. P->(P->P). Instances of A1.
5. P->P. MP: 3,4.
 
I was reading documentation about the soundness and completeness of logic formal systems. Consider the following $$\vdash_S \phi$$ where ##S## is the proof-system making part the formal system and ##\phi## is a wff (well formed formula) of the formal language. Note the blank on left of the turnstile symbol ##\vdash_S##, as far as I can tell it actually represents the empty set. So what does it mean ? I guess it actually means ##\phi## is a theorem of the formal system, i.e. there is a...

Similar threads

Back
Top