Mixing
Why can't we generally replace inference rules with axioms?
Clash Royale CLAN TAG#URR8PPP
up vote
5
down vote
favorite
Is there a big difference in having insufficient axioms and insufficient inference rules/proof procedure to have a complete theory?
It seems like in many cases adding a new inference rule or a new axiom has the same effect. For example, consider a language with 2-place connectives $rightarrow, land$. The language also has an inference rule $arightarrow b,a Longrightarrow b$.
Now we can add a new axiom schemes: $aland b rightarrow a$ and $a land brightarrow b$ for any formula $a,b$. An alternative is to add a new inference rules: $aland b Longrightarrow a$ and $aland b Longrightarrow b$. In this case I claim the theories are equivalent no matter the axiomatization.
In particular, I would think that in second order logic something prevents us from replacing inference rules with axioms, no matter how many inference rules are defined, since it is stated that second order proof calculus is always insufficient (for certain theories). Otherwise we could always use the same proof calculus and merely add axioms, and thus have a universal proof checking procedure. Why does adding axioms in place of inference rules fail?
logic proof-theory second-order-logic
edited Jul 23 at 22:27
Taroccoesbrocco
3,48941431
asked Jul 23 at 21:51
Dole
792514
add a comment |Â
up vote
5
down vote
favorite
Is there a big difference in having insufficient axioms and insufficient inference rules/proof procedure to have a complete theory?
It seems like in many cases adding a new inference rule or a new axiom has the same effect. For example, consider a language with 2-place connectives $rightarrow, land$. The language also has an inference rule $arightarrow b,a Longrightarrow b$.
Now we can add a new axiom schemes: $aland b rightarrow a$ and $a land brightarrow b$ for any formula $a,b$. An alternative is to add a new inference rules: $aland b Longrightarrow a$ and $aland b Longrightarrow b$. In this case I claim the theories are equivalent no matter the axiomatization.
In particular, I would think that in second order logic something prevents us from replacing inference rules with axioms, no matter how many inference rules are defined, since it is stated that second order proof calculus is always insufficient (for certain theories). Otherwise we could always use the same proof calculus and merely add axioms, and thus have a universal proof checking procedure. Why does adding axioms in place of inference rules fail?
logic proof-theory second-order-logic
edited Jul 23 at 22:27
Taroccoesbrocco
3,48941431
asked Jul 23 at 21:51
Dole
792514
"Now we can add a new axiom schemes: a∧b→a and a∧b→b for any formula a,b. An alternative is to add a new inference rules: a∧b⟹a and a∧b⟹b. In this case I claim the theories are equivalent no matter the axiomatization." No. If you add the axioms ((a∧b)⟹a) and ((a∧b)⟹b), then the inference rules (a∧b)⟹a and (a∧b)⟹b are derivable because of your detachment rule of inference. But, it doesn't follow from the detachment rule that if you add the inference rules above, that the above formulas are theorems. Consequently, this question seems backwards. It's "why can't we replace axioms with rules?"
– Doug Spoonwood
Jul 23 at 22:35
3
I don't understand what you think replacing inference rules with axioms has to do with making second-order logic complete. Are you just proposing to add a new axiom for every single semantically valid inference?
– Eric Wofsey
Jul 24 at 0:17
Related
– Henning Makholm
Jul 24 at 0:57
add a comment |Â
up vote
5
down vote
favorite
up vote
5
down vote
favorite
Is there a big difference in having insufficient axioms and insufficient inference rules/proof procedure to have a complete theory?
It seems like in many cases adding a new inference rule or a new axiom has the same effect. For example, consider a language with 2-place connectives $rightarrow, land$. The language also has an inference rule $arightarrow b,a Longrightarrow b$.
Now we can add a new axiom schemes: $aland b rightarrow a$ and $a land brightarrow b$ for any formula $a,b$. An alternative is to add a new inference rules: $aland b Longrightarrow a$ and $aland b Longrightarrow b$. In this case I claim the theories are equivalent no matter the axiomatization.
In particular, I would think that in second order logic something prevents us from replacing inference rules with axioms, no matter how many inference rules are defined, since it is stated that second order proof calculus is always insufficient (for certain theories). Otherwise we could always use the same proof calculus and merely add axioms, and thus have a universal proof checking procedure. Why does adding axioms in place of inference rules fail?
logic proof-theory second-order-logic
edited Jul 23 at 22:27
Taroccoesbrocco
3,48941431
asked Jul 23 at 21:51
Dole
792514
Is there a big difference in having insufficient axioms and insufficient inference rules/proof procedure to have a complete theory?
It seems like in many cases adding a new inference rule or a new axiom has the same effect. For example, consider a language with 2-place connectives $rightarrow, land$. The language also has an inference rule $arightarrow b,a Longrightarrow b$.
Now we can add a new axiom schemes: $aland b rightarrow a$ and $a land brightarrow b$ for any formula $a,b$. An alternative is to add a new inference rules: $aland b Longrightarrow a$ and $aland b Longrightarrow b$. In this case I claim the theories are equivalent no matter the axiomatization.
In particular, I would think that in second order logic something prevents us from replacing inference rules with axioms, no matter how many inference rules are defined, since it is stated that second order proof calculus is always insufficient (for certain theories). Otherwise we could always use the same proof calculus and merely add axioms, and thus have a universal proof checking procedure. Why does adding axioms in place of inference rules fail?
logic proof-theory second-order-logic
edited Jul 23 at 22:27
Taroccoesbrocco
3,48941431
asked Jul 23 at 21:51
Dole
792514
edited Jul 23 at 22:27
Taroccoesbrocco
3,48941431
edited Jul 23 at 22:27
Taroccoesbrocco
3,48941431
edited Jul 23 at 22:27
Taroccoesbrocco
3,48941431
3,48941431
asked Jul 23 at 21:51
Dole
792514
asked Jul 23 at 21:51
Dole
792514
asked Jul 23 at 21:51
Dole
792514
792514
"Now we can add a new axiom schemes: a∧b→a and a∧b→b for any formula a,b. An alternative is to add a new inference rules: a∧b⟹a and a∧b⟹b. In this case I claim the theories are equivalent no matter the axiomatization." No. If you add the axioms ((a∧b)⟹a) and ((a∧b)⟹b), then the inference rules (a∧b)⟹a and (a∧b)⟹b are derivable because of your detachment rule of inference. But, it doesn't follow from the detachment rule that if you add the inference rules above, that the above formulas are theorems. Consequently, this question seems backwards. It's "why can't we replace axioms with rules?"
– Doug Spoonwood
Jul 23 at 22:35
3
I don't understand what you think replacing inference rules with axioms has to do with making second-order logic complete. Are you just proposing to add a new axiom for every single semantically valid inference?
– Eric Wofsey
Jul 24 at 0:17
Related
– Henning Makholm
Jul 24 at 0:57
add a comment |Â
"Now we can add a new axiom schemes: a∧b→a and a∧b→b for any formula a,b. An alternative is to add a new inference rules: a∧b⟹a and a∧b⟹b. In this case I claim the theories are equivalent no matter the axiomatization." No. If you add the axioms ((a∧b)⟹a) and ((a∧b)⟹b), then the inference rules (a∧b)⟹a and (a∧b)⟹b are derivable because of your detachment rule of inference. But, it doesn't follow from the detachment rule that if you add the inference rules above, that the above formulas are theorems. Consequently, this question seems backwards. It's "why can't we replace axioms with rules?"
– Doug Spoonwood
Jul 23 at 22:35
3
I don't understand what you think replacing inference rules with axioms has to do with making second-order logic complete. Are you just proposing to add a new axiom for every single semantically valid inference?
– Eric Wofsey
Jul 24 at 0:17
Related
– Henning Makholm
Jul 24 at 0:57
"Now we can add a new axiom schemes: a∧b→a and a∧b→b for any formula a,b. An alternative is to add a new inference rules: a∧b⟹a and a∧b⟹b. In this case I claim the theories are equivalent no matter the axiomatization." No. If you add the axioms ((a∧b)⟹a) and ((a∧b)⟹b), then the inference rules (a∧b)⟹a and (a∧b)⟹b are derivable because of your detachment rule of inference. But, it doesn't follow from the detachment rule that if you add the inference rules above, that the above formulas are theorems. Consequently, this question seems backwards. It's "why can't we replace axioms with rules?"
– Doug Spoonwood
Jul 23 at 22:35
"Now we can add a new axiom schemes: a∧b→a and a∧b→b for any formula a,b. An alternative is to add a new inference rules: a∧b⟹a and a∧b⟹b. In this case I claim the theories are equivalent no matter the axiomatization." No. If you add the axioms ((a∧b)⟹a) and ((a∧b)⟹b), then the inference rules (a∧b)⟹a and (a∧b)⟹b are derivable because of your detachment rule of inference. But, it doesn't follow from the detachment rule that if you add the inference rules above, that the above formulas are theorems. Consequently, this question seems backwards. It's "why can't we replace axioms with rules?"
– Doug Spoonwood
Jul 23 at 22:35
3
3
I don't understand what you think replacing inference rules with axioms has to do with making second-order logic complete. Are you just proposing to add a new axiom for every single semantically valid inference?
– Eric Wofsey
Jul 24 at 0:17
I don't understand what you think replacing inference rules with axioms has to do with making second-order logic complete. Are you just proposing to add a new axiom for every single semantically valid inference?
– Eric Wofsey
Jul 24 at 0:17
Related
– Henning Makholm
Jul 24 at 0:57
Related
– Henning Makholm
Jul 24 at 0:57
add a comment |Â
1 Answer
1
active
oldest
votes
up vote
0
down vote
Axioms, Axiom Schemas, and Rules of Inferences are 3 different things.
An axiom is a piece of data. It is a proposition that is introduced to a logic without proof.
A Rule of Inference (RoI) is a program. It can be thought of as a program to generate a new proposition from existing propositions (enumeration); it can be thought of as a decision procedure to check if a new proposition follows from existing propositions (verification).
An Axiom Schema is an RoI that introduces a countably infinite number of propositions. So the description of an axiom schema as $(A land B) to A$ introduces $(X land X) to X$, $(x > y land y > z) to (x > z)$, etc, all to the theory.
Some logics explicitly have an RoI named "Propositional Substition". This is the rule that if you have a propositional expression proven, any propositional variable can be completely replaced by an arbitrary propositional expression. So for example, if you have proven $(X to X)$, then you can infer $((A lor B) to (A lor B))$. Jaśkowski made this rule explicit in his logic.
In a logic with Propositional Substition, Axioms and Axiom Schema of the same description induce the same theory. In fact, such logics tend to not even bother with Axiom Schema. In a logic without Propositional Substitution, then Axioms and Axiom Schema of the same description can induce different theories. For example, from the axiom $X to X$ you could not infer $Y to Y $ without Propositional Substitution.
Eliminating all RoI (even just those that are not Axiom Schema) would make it impossible to introduce new theorems to the theory, so you would never be able to prove anything except what is explicitly assumed.
In modern logic, a hot question tends to actually be the exact opposite: how can we make it so that user of a logic can introduce new valid RoI? There are a lot of decision procedures that can evaluate propositions and decide their correctness much faster than being restricted to compositions of a few hardcoded RoI, and as formal libraries get larger, this becomes a major bottleneck.
answered Jul 23 at 23:11
DanielV
17.4k42651
2
I don't entirely understand the question (and I don't think OP does either), but I'm pretty sure that this is not an answer to it at all. As far as I can tell the real question here is "what does it mean that second-order logic has no good proof system?".
– Eric Wofsey
Jul 23 at 23:29
He is asking 2 different questions, the first half and the second half are pretty unrelated IMO. The first half is what I'm addressing here.
– DanielV
Jul 23 at 23:32
@EricWofsey That means that there is a formula that is true in all the models, but can not be proven. This means we can discover new truths by adding inference rules. But, why not just settle on some inference rules and rather add axioms as needed? Then there is a universal proof verification procedure... and second order logic behaves more like the first order where only the axiomatic incompletness is the problem (as the proof calculus is complete for FO). I feel there must be a reason why adding (consistent) axioms thus can't replace adding inference rules, and am asking why?
– Dole
Jul 24 at 1:26
@Dole: Adding axioms is completely interchangeable with adding inference rules. No one cares about either approach because neither one actually solves the real problem with proofs in second-order logic.
– Eric Wofsey
Jul 24 at 1:37
A "univeral proof verification procedure" is useless if you can't even verify what your logical axioms are.
– Eric Wofsey
Jul 24 at 1:41
 |Â
show 1 more comment
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
up vote
0
down vote
Axioms, Axiom Schemas, and Rules of Inferences are 3 different things.
An axiom is a piece of data. It is a proposition that is introduced to a logic without proof.
A Rule of Inference (RoI) is a program. It can be thought of as a program to generate a new proposition from existing propositions (enumeration); it can be thought of as a decision procedure to check if a new proposition follows from existing propositions (verification).
An Axiom Schema is an RoI that introduces a countably infinite number of propositions. So the description of an axiom schema as $(A land B) to A$ introduces $(X land X) to X$, $(x > y land y > z) to (x > z)$, etc, all to the theory.
Some logics explicitly have an RoI named "Propositional Substition". This is the rule that if you have a propositional expression proven, any propositional variable can be completely replaced by an arbitrary propositional expression. So for example, if you have proven $(X to X)$, then you can infer $((A lor B) to (A lor B))$. Jaśkowski made this rule explicit in his logic.
In a logic with Propositional Substition, Axioms and Axiom Schema of the same description induce the same theory. In fact, such logics tend to not even bother with Axiom Schema. In a logic without Propositional Substitution, then Axioms and Axiom Schema of the same description can induce different theories. For example, from the axiom $X to X$ you could not infer $Y to Y $ without Propositional Substitution.
Eliminating all RoI (even just those that are not Axiom Schema) would make it impossible to introduce new theorems to the theory, so you would never be able to prove anything except what is explicitly assumed.
In modern logic, a hot question tends to actually be the exact opposite: how can we make it so that user of a logic can introduce new valid RoI? There are a lot of decision procedures that can evaluate propositions and decide their correctness much faster than being restricted to compositions of a few hardcoded RoI, and as formal libraries get larger, this becomes a major bottleneck.
answered Jul 23 at 23:11
DanielV
17.4k42651
2
I don't entirely understand the question (and I don't think OP does either), but I'm pretty sure that this is not an answer to it at all. As far as I can tell the real question here is "what does it mean that second-order logic has no good proof system?".
– Eric Wofsey
Jul 23 at 23:29
He is asking 2 different questions, the first half and the second half are pretty unrelated IMO. The first half is what I'm addressing here.
– DanielV
Jul 23 at 23:32
@EricWofsey That means that there is a formula that is true in all the models, but can not be proven. This means we can discover new truths by adding inference rules. But, why not just settle on some inference rules and rather add axioms as needed? Then there is a universal proof verification procedure... and second order logic behaves more like the first order where only the axiomatic incompletness is the problem (as the proof calculus is complete for FO). I feel there must be a reason why adding (consistent) axioms thus can't replace adding inference rules, and am asking why?
– Dole
Jul 24 at 1:26
@Dole: Adding axioms is completely interchangeable with adding inference rules. No one cares about either approach because neither one actually solves the real problem with proofs in second-order logic.
– Eric Wofsey
Jul 24 at 1:37
A "univeral proof verification procedure" is useless if you can't even verify what your logical axioms are.
– Eric Wofsey
Jul 24 at 1:41
 |Â
show 1 more comment
up vote
0
down vote
Axioms, Axiom Schemas, and Rules of Inferences are 3 different things.
An axiom is a piece of data. It is a proposition that is introduced to a logic without proof.
A Rule of Inference (RoI) is a program. It can be thought of as a program to generate a new proposition from existing propositions (enumeration); it can be thought of as a decision procedure to check if a new proposition follows from existing propositions (verification).
An Axiom Schema is an RoI that introduces a countably infinite number of propositions. So the description of an axiom schema as $(A land B) to A$ introduces $(X land X) to X$, $(x > y land y > z) to (x > z)$, etc, all to the theory.
Some logics explicitly have an RoI named "Propositional Substition". This is the rule that if you have a propositional expression proven, any propositional variable can be completely replaced by an arbitrary propositional expression. So for example, if you have proven $(X to X)$, then you can infer $((A lor B) to (A lor B))$. Jaśkowski made this rule explicit in his logic.
In a logic with Propositional Substition, Axioms and Axiom Schema of the same description induce the same theory. In fact, such logics tend to not even bother with Axiom Schema. In a logic without Propositional Substitution, then Axioms and Axiom Schema of the same description can induce different theories. For example, from the axiom $X to X$ you could not infer $Y to Y $ without Propositional Substitution.
Eliminating all RoI (even just those that are not Axiom Schema) would make it impossible to introduce new theorems to the theory, so you would never be able to prove anything except what is explicitly assumed.
In modern logic, a hot question tends to actually be the exact opposite: how can we make it so that user of a logic can introduce new valid RoI? There are a lot of decision procedures that can evaluate propositions and decide their correctness much faster than being restricted to compositions of a few hardcoded RoI, and as formal libraries get larger, this becomes a major bottleneck.
answered Jul 23 at 23:11
DanielV
17.4k42651
2
I don't entirely understand the question (and I don't think OP does either), but I'm pretty sure that this is not an answer to it at all. As far as I can tell the real question here is "what does it mean that second-order logic has no good proof system?".
– Eric Wofsey
Jul 23 at 23:29
He is asking 2 different questions, the first half and the second half are pretty unrelated IMO. The first half is what I'm addressing here.
– DanielV
Jul 23 at 23:32
@EricWofsey That means that there is a formula that is true in all the models, but can not be proven. This means we can discover new truths by adding inference rules. But, why not just settle on some inference rules and rather add axioms as needed? Then there is a universal proof verification procedure... and second order logic behaves more like the first order where only the axiomatic incompletness is the problem (as the proof calculus is complete for FO). I feel there must be a reason why adding (consistent) axioms thus can't replace adding inference rules, and am asking why?
– Dole
Jul 24 at 1:26
@Dole: Adding axioms is completely interchangeable with adding inference rules. No one cares about either approach because neither one actually solves the real problem with proofs in second-order logic.
– Eric Wofsey
Jul 24 at 1:37
A "univeral proof verification procedure" is useless if you can't even verify what your logical axioms are.
– Eric Wofsey
Jul 24 at 1:41
 |Â
show 1 more comment
up vote
0
down vote
up vote
0
down vote
Axioms, Axiom Schemas, and Rules of Inferences are 3 different things.
An axiom is a piece of data. It is a proposition that is introduced to a logic without proof.
A Rule of Inference (RoI) is a program. It can be thought of as a program to generate a new proposition from existing propositions (enumeration); it can be thought of as a decision procedure to check if a new proposition follows from existing propositions (verification).
An Axiom Schema is an RoI that introduces a countably infinite number of propositions. So the description of an axiom schema as $(A land B) to A$ introduces $(X land X) to X$, $(x > y land y > z) to (x > z)$, etc, all to the theory.
Some logics explicitly have an RoI named "Propositional Substition". This is the rule that if you have a propositional expression proven, any propositional variable can be completely replaced by an arbitrary propositional expression. So for example, if you have proven $(X to X)$, then you can infer $((A lor B) to (A lor B))$. Jaśkowski made this rule explicit in his logic.
In a logic with Propositional Substition, Axioms and Axiom Schema of the same description induce the same theory. In fact, such logics tend to not even bother with Axiom Schema. In a logic without Propositional Substitution, then Axioms and Axiom Schema of the same description can induce different theories. For example, from the axiom $X to X$ you could not infer $Y to Y $ without Propositional Substitution.
Eliminating all RoI (even just those that are not Axiom Schema) would make it impossible to introduce new theorems to the theory, so you would never be able to prove anything except what is explicitly assumed.
In modern logic, a hot question tends to actually be the exact opposite: how can we make it so that user of a logic can introduce new valid RoI? There are a lot of decision procedures that can evaluate propositions and decide their correctness much faster than being restricted to compositions of a few hardcoded RoI, and as formal libraries get larger, this becomes a major bottleneck.
answered Jul 23 at 23:11
DanielV
17.4k42651
Axioms, Axiom Schemas, and Rules of Inferences are 3 different things.
An axiom is a piece of data. It is a proposition that is introduced to a logic without proof.
A Rule of Inference (RoI) is a program. It can be thought of as a program to generate a new proposition from existing propositions (enumeration); it can be thought of as a decision procedure to check if a new proposition follows from existing propositions (verification).
An Axiom Schema is an RoI that introduces a countably infinite number of propositions. So the description of an axiom schema as $(A land B) to A$ introduces $(X land X) to X$, $(x > y land y > z) to (x > z)$, etc, all to the theory.
Some logics explicitly have an RoI named "Propositional Substition". This is the rule that if you have a propositional expression proven, any propositional variable can be completely replaced by an arbitrary propositional expression. So for example, if you have proven $(X to X)$, then you can infer $((A lor B) to (A lor B))$. Jaśkowski made this rule explicit in his logic.
In a logic with Propositional Substition, Axioms and Axiom Schema of the same description induce the same theory. In fact, such logics tend to not even bother with Axiom Schema. In a logic without Propositional Substitution, then Axioms and Axiom Schema of the same description can induce different theories. For example, from the axiom $X to X$ you could not infer $Y to Y $ without Propositional Substitution.
Eliminating all RoI (even just those that are not Axiom Schema) would make it impossible to introduce new theorems to the theory, so you would never be able to prove anything except what is explicitly assumed.
In modern logic, a hot question tends to actually be the exact opposite: how can we make it so that user of a logic can introduce new valid RoI? There are a lot of decision procedures that can evaluate propositions and decide their correctness much faster than being restricted to compositions of a few hardcoded RoI, and as formal libraries get larger, this becomes a major bottleneck.
answered Jul 23 at 23:11
DanielV
17.4k42651
answered Jul 23 at 23:11
DanielV
17.4k42651
answered Jul 23 at 23:11
DanielV
17.4k42651
answered Jul 23 at 23:11
DanielV
17.4k42651
17.4k42651
2
I don't entirely understand the question (and I don't think OP does either), but I'm pretty sure that this is not an answer to it at all. As far as I can tell the real question here is "what does it mean that second-order logic has no good proof system?".
– Eric Wofsey
Jul 23 at 23:29
He is asking 2 different questions, the first half and the second half are pretty unrelated IMO. The first half is what I'm addressing here.
– DanielV
Jul 23 at 23:32
@EricWofsey That means that there is a formula that is true in all the models, but can not be proven. This means we can discover new truths by adding inference rules. But, why not just settle on some inference rules and rather add axioms as needed? Then there is a universal proof verification procedure... and second order logic behaves more like the first order where only the axiomatic incompletness is the problem (as the proof calculus is complete for FO). I feel there must be a reason why adding (consistent) axioms thus can't replace adding inference rules, and am asking why?
– Dole
Jul 24 at 1:26
@Dole: Adding axioms is completely interchangeable with adding inference rules. No one cares about either approach because neither one actually solves the real problem with proofs in second-order logic.
– Eric Wofsey
Jul 24 at 1:37
A "univeral proof verification procedure" is useless if you can't even verify what your logical axioms are.
– Eric Wofsey
Jul 24 at 1:41
 |Â
show 1 more comment
2
I don't entirely understand the question (and I don't think OP does either), but I'm pretty sure that this is not an answer to it at all. As far as I can tell the real question here is "what does it mean that second-order logic has no good proof system?".
– Eric Wofsey
Jul 23 at 23:29
He is asking 2 different questions, the first half and the second half are pretty unrelated IMO. The first half is what I'm addressing here.
– DanielV
Jul 23 at 23:32
@EricWofsey That means that there is a formula that is true in all the models, but can not be proven. This means we can discover new truths by adding inference rules. But, why not just settle on some inference rules and rather add axioms as needed? Then there is a universal proof verification procedure... and second order logic behaves more like the first order where only the axiomatic incompletness is the problem (as the proof calculus is complete for FO). I feel there must be a reason why adding (consistent) axioms thus can't replace adding inference rules, and am asking why?
– Dole
Jul 24 at 1:26
@Dole: Adding axioms is completely interchangeable with adding inference rules. No one cares about either approach because neither one actually solves the real problem with proofs in second-order logic.
– Eric Wofsey
Jul 24 at 1:37
A "univeral proof verification procedure" is useless if you can't even verify what your logical axioms are.
– Eric Wofsey
Jul 24 at 1:41
2
2
I don't entirely understand the question (and I don't think OP does either), but I'm pretty sure that this is not an answer to it at all. As far as I can tell the real question here is "what does it mean that second-order logic has no good proof system?".
– Eric Wofsey
Jul 23 at 23:29
I don't entirely understand the question (and I don't think OP does either), but I'm pretty sure that this is not an answer to it at all. As far as I can tell the real question here is "what does it mean that second-order logic has no good proof system?".
– Eric Wofsey
Jul 23 at 23:29
He is asking 2 different questions, the first half and the second half are pretty unrelated IMO. The first half is what I'm addressing here.
– DanielV
Jul 23 at 23:32
He is asking 2 different questions, the first half and the second half are pretty unrelated IMO. The first half is what I'm addressing here.
– DanielV
Jul 23 at 23:32
@EricWofsey That means that there is a formula that is true in all the models, but can not be proven. This means we can discover new truths by adding inference rules. But, why not just settle on some inference rules and rather add axioms as needed? Then there is a universal proof verification procedure... and second order logic behaves more like the first order where only the axiomatic incompletness is the problem (as the proof calculus is complete for FO). I feel there must be a reason why adding (consistent) axioms thus can't replace adding inference rules, and am asking why?
– Dole
Jul 24 at 1:26
@EricWofsey That means that there is a formula that is true in all the models, but can not be proven. This means we can discover new truths by adding inference rules. But, why not just settle on some inference rules and rather add axioms as needed? Then there is a universal proof verification procedure... and second order logic behaves more like the first order where only the axiomatic incompletness is the problem (as the proof calculus is complete for FO). I feel there must be a reason why adding (consistent) axioms thus can't replace adding inference rules, and am asking why?
– Dole
Jul 24 at 1:26
@Dole: Adding axioms is completely interchangeable with adding inference rules. No one cares about either approach because neither one actually solves the real problem with proofs in second-order logic.
– Eric Wofsey
Jul 24 at 1:37
@Dole: Adding axioms is completely interchangeable with adding inference rules. No one cares about either approach because neither one actually solves the real problem with proofs in second-order logic.
– Eric Wofsey
Jul 24 at 1:37
A "univeral proof verification procedure" is useless if you can't even verify what your logical axioms are.
– Eric Wofsey
Jul 24 at 1:41
A "univeral proof verification procedure" is useless if you can't even verify what your logical axioms are.
– Eric Wofsey
Jul 24 at 1:41
 |Â
show 1 more comment
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
StackExchange.ready(
function ()
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f2860811%2fwhy-cant-we-generally-replace-inference-rules-with-axioms%23new-answer', 'question_page');
);
Post as a guest
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
"Now we can add a new axiom schemes: a∧b→a and a∧b→b for any formula a,b. An alternative is to add a new inference rules: a∧b⟹a and a∧b⟹b. In this case I claim the theories are equivalent no matter the axiomatization." No. If you add the axioms ((a∧b)⟹a) and ((a∧b)⟹b), then the inference rules (a∧b)⟹a and (a∧b)⟹b are derivable because of your detachment rule of inference. But, it doesn't follow from the detachment rule that if you add the inference rules above, that the above formulas are theorems. Consequently, this question seems backwards. It's "why can't we replace axioms with rules?"
– Doug Spoonwood
Jul 23 at 22:35
3
I don't understand what you think replacing inference rules with axioms has to do with making second-order logic complete. Are you just proposing to add a new axiom for every single semantically valid inference?
– Eric Wofsey
Jul 24 at 0:17
Related
– Henning Makholm
Jul 24 at 0:57