Mixing
Are there logical systems where formal proofs are not computer verifiable?
Clash Royale CLAN TAG#URR8PPP
up vote
1
down vote
favorite
In a set-theoretic system using first-order logic, every proof could be written as a goal followed by a finite sequence of sentence where each one is justified by an axiom or previously established sentence and the last line is the goal. Computers can easily verify proofs like these using the rules of first-order logic.
In dependent type theory, proofs come in the form of programs, and you know your proof is correct if it can be compiled (or type-checked).
Do there exist logics/foundations where rigorous proofs can not be checked by computers? Or where a checking program might never terminate for a correct proof?
lo.logic computer-science foundations
asked 5 hours ago
Eben Cowley
1184
 |Â
show 1 more comment
up vote
1
down vote
favorite
In a set-theoretic system using first-order logic, every proof could be written as a goal followed by a finite sequence of sentence where each one is justified by an axiom or previously established sentence and the last line is the goal. Computers can easily verify proofs like these using the rules of first-order logic.
In dependent type theory, proofs come in the form of programs, and you know your proof is correct if it can be compiled (or type-checked).
Do there exist logics/foundations where rigorous proofs can not be checked by computers? Or where a checking program might never terminate for a correct proof?
lo.logic computer-science foundations
asked 5 hours ago
Eben Cowley
1184
And a "rigorous" proof is what exactly? And by computer you mean physical computers or theoretical computers such as Turing machines?
– Somos
4 hours ago
If a proof does not have a verification process, what use is the proof? Or are you imagining something that resembles a proof in some ways and not in others? Gerhard "Too Philosophical For This Forum?" Paseman, 2018.10.10.
– Gerhard Paseman
4 hours ago
@Somos I mean theoretical computers. I left the notion of rigor undefined because I'm curious if there are systems which define it in a way that isn't computationally verifiable.
– Eben Cowley
4 hours ago
@GerhardPaseman Good question, I'm not sure how such proofs could be considered proofs, which is why I'm so curious about it. Perhaps it's my post that is too philosophical for the forum, but this seemed like the site where it would be the most likely to get an answer.
– Eben Cowley
3 hours ago
This post may answer your question: math.andrej.com/2016/08/09/what-is-a-formal-proof
– L. Garde
3 hours ago
 |Â
show 1 more comment
up vote
1
down vote
favorite
up vote
1
down vote
favorite
In a set-theoretic system using first-order logic, every proof could be written as a goal followed by a finite sequence of sentence where each one is justified by an axiom or previously established sentence and the last line is the goal. Computers can easily verify proofs like these using the rules of first-order logic.
In dependent type theory, proofs come in the form of programs, and you know your proof is correct if it can be compiled (or type-checked).
Do there exist logics/foundations where rigorous proofs can not be checked by computers? Or where a checking program might never terminate for a correct proof?
lo.logic computer-science foundations
asked 5 hours ago
Eben Cowley
1184
In a set-theoretic system using first-order logic, every proof could be written as a goal followed by a finite sequence of sentence where each one is justified by an axiom or previously established sentence and the last line is the goal. Computers can easily verify proofs like these using the rules of first-order logic.
In dependent type theory, proofs come in the form of programs, and you know your proof is correct if it can be compiled (or type-checked).
Do there exist logics/foundations where rigorous proofs can not be checked by computers? Or where a checking program might never terminate for a correct proof?
lo.logic computer-science foundations
lo.logic computer-science foundations
asked 5 hours ago
Eben Cowley
1184
asked 5 hours ago
Eben Cowley
1184
asked 5 hours ago
Eben Cowley
1184
asked 5 hours ago
Eben Cowley
1184
asked 5 hours ago
Eben Cowley
1184
1184
And a "rigorous" proof is what exactly? And by computer you mean physical computers or theoretical computers such as Turing machines?
– Somos
4 hours ago
If a proof does not have a verification process, what use is the proof? Or are you imagining something that resembles a proof in some ways and not in others? Gerhard "Too Philosophical For This Forum?" Paseman, 2018.10.10.
– Gerhard Paseman
4 hours ago
@Somos I mean theoretical computers. I left the notion of rigor undefined because I'm curious if there are systems which define it in a way that isn't computationally verifiable.
– Eben Cowley
4 hours ago
@GerhardPaseman Good question, I'm not sure how such proofs could be considered proofs, which is why I'm so curious about it. Perhaps it's my post that is too philosophical for the forum, but this seemed like the site where it would be the most likely to get an answer.
– Eben Cowley
3 hours ago
This post may answer your question: math.andrej.com/2016/08/09/what-is-a-formal-proof
– L. Garde
3 hours ago
 |Â
show 1 more comment
And a "rigorous" proof is what exactly? And by computer you mean physical computers or theoretical computers such as Turing machines?
– Somos
4 hours ago
If a proof does not have a verification process, what use is the proof? Or are you imagining something that resembles a proof in some ways and not in others? Gerhard "Too Philosophical For This Forum?" Paseman, 2018.10.10.
– Gerhard Paseman
4 hours ago
@Somos I mean theoretical computers. I left the notion of rigor undefined because I'm curious if there are systems which define it in a way that isn't computationally verifiable.
– Eben Cowley
4 hours ago
@GerhardPaseman Good question, I'm not sure how such proofs could be considered proofs, which is why I'm so curious about it. Perhaps it's my post that is too philosophical for the forum, but this seemed like the site where it would be the most likely to get an answer.
– Eben Cowley
3 hours ago
This post may answer your question: math.andrej.com/2016/08/09/what-is-a-formal-proof
– L. Garde
3 hours ago
And a "rigorous" proof is what exactly? And by computer you mean physical computers or theoretical computers such as Turing machines?
– Somos
4 hours ago
And a "rigorous" proof is what exactly? And by computer you mean physical computers or theoretical computers such as Turing machines?
– Somos
4 hours ago
If a proof does not have a verification process, what use is the proof? Or are you imagining something that resembles a proof in some ways and not in others? Gerhard "Too Philosophical For This Forum?" Paseman, 2018.10.10.
– Gerhard Paseman
4 hours ago
If a proof does not have a verification process, what use is the proof? Or are you imagining something that resembles a proof in some ways and not in others? Gerhard "Too Philosophical For This Forum?" Paseman, 2018.10.10.
– Gerhard Paseman
4 hours ago
@Somos I mean theoretical computers. I left the notion of rigor undefined because I'm curious if there are systems which define it in a way that isn't computationally verifiable.
– Eben Cowley
4 hours ago
@Somos I mean theoretical computers. I left the notion of rigor undefined because I'm curious if there are systems which define it in a way that isn't computationally verifiable.
– Eben Cowley
4 hours ago
@GerhardPaseman Good question, I'm not sure how such proofs could be considered proofs, which is why I'm so curious about it. Perhaps it's my post that is too philosophical for the forum, but this seemed like the site where it would be the most likely to get an answer.
– Eben Cowley
3 hours ago
@GerhardPaseman Good question, I'm not sure how such proofs could be considered proofs, which is why I'm so curious about it. Perhaps it's my post that is too philosophical for the forum, but this seemed like the site where it would be the most likely to get an answer.
– Eben Cowley
3 hours ago
This post may answer your question: math.andrej.com/2016/08/09/what-is-a-formal-proof
– L. Garde
3 hours ago
This post may answer your question: math.andrej.com/2016/08/09/what-is-a-formal-proof
– L. Garde
3 hours ago
 |Â
show 1 more comment
1 Answer
1
active
oldest
votes
up vote
4
down vote
There are logical systems whose formal proofs are not computer verifiable. One such example is infinitary logic in which logical statements can be infinitely long, and a specific statement in a proof may require infinitely many premises to be checked. Such logical systems have their value in studying various aspects of foundations of mathematics, but are not normally considered to properly reflect the actual human activity of proving mathematical statements.
All logical systems (first-order logic, higher-order logic, type theory, etc.) whose purpose is to capture the notion of proof as done in practice, have machine verifiable proofs. The formal property needed here is semidecidability.
answered 1 hour ago
Andrej Bauer
28.4k474156
add a comment |Â
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
up vote
4
down vote
There are logical systems whose formal proofs are not computer verifiable. One such example is infinitary logic in which logical statements can be infinitely long, and a specific statement in a proof may require infinitely many premises to be checked. Such logical systems have their value in studying various aspects of foundations of mathematics, but are not normally considered to properly reflect the actual human activity of proving mathematical statements.
All logical systems (first-order logic, higher-order logic, type theory, etc.) whose purpose is to capture the notion of proof as done in practice, have machine verifiable proofs. The formal property needed here is semidecidability.
answered 1 hour ago
Andrej Bauer
28.4k474156
add a comment |Â
up vote
4
down vote
There are logical systems whose formal proofs are not computer verifiable. One such example is infinitary logic in which logical statements can be infinitely long, and a specific statement in a proof may require infinitely many premises to be checked. Such logical systems have their value in studying various aspects of foundations of mathematics, but are not normally considered to properly reflect the actual human activity of proving mathematical statements.
All logical systems (first-order logic, higher-order logic, type theory, etc.) whose purpose is to capture the notion of proof as done in practice, have machine verifiable proofs. The formal property needed here is semidecidability.
answered 1 hour ago
Andrej Bauer
28.4k474156
add a comment |Â
up vote
4
down vote
up vote
4
down vote
There are logical systems whose formal proofs are not computer verifiable. One such example is infinitary logic in which logical statements can be infinitely long, and a specific statement in a proof may require infinitely many premises to be checked. Such logical systems have their value in studying various aspects of foundations of mathematics, but are not normally considered to properly reflect the actual human activity of proving mathematical statements.
All logical systems (first-order logic, higher-order logic, type theory, etc.) whose purpose is to capture the notion of proof as done in practice, have machine verifiable proofs. The formal property needed here is semidecidability.
answered 1 hour ago
Andrej Bauer
28.4k474156
There are logical systems whose formal proofs are not computer verifiable. One such example is infinitary logic in which logical statements can be infinitely long, and a specific statement in a proof may require infinitely many premises to be checked. Such logical systems have their value in studying various aspects of foundations of mathematics, but are not normally considered to properly reflect the actual human activity of proving mathematical statements.
All logical systems (first-order logic, higher-order logic, type theory, etc.) whose purpose is to capture the notion of proof as done in practice, have machine verifiable proofs. The formal property needed here is semidecidability.
answered 1 hour ago
Andrej Bauer
28.4k474156
answered 1 hour ago
Andrej Bauer
28.4k474156
answered 1 hour ago
Andrej Bauer
28.4k474156
answered 1 hour ago
Andrej Bauer
28.4k474156
28.4k474156
add a comment |Â
add a 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%2fmathoverflow.net%2fquestions%2f312533%2fare-there-logical-systems-where-formal-proofs-are-not-computer-verifiable%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
And a "rigorous" proof is what exactly? And by computer you mean physical computers or theoretical computers such as Turing machines?
– Somos
4 hours ago
If a proof does not have a verification process, what use is the proof? Or are you imagining something that resembles a proof in some ways and not in others? Gerhard "Too Philosophical For This Forum?" Paseman, 2018.10.10.
– Gerhard Paseman
4 hours ago
@Somos I mean theoretical computers. I left the notion of rigor undefined because I'm curious if there are systems which define it in a way that isn't computationally verifiable.
– Eben Cowley
4 hours ago
@GerhardPaseman Good question, I'm not sure how such proofs could be considered proofs, which is why I'm so curious about it. Perhaps it's my post that is too philosophical for the forum, but this seemed like the site where it would be the most likely to get an answer.
– Eben Cowley
3 hours ago
This post may answer your question: math.andrej.com/2016/08/09/what-is-a-formal-proof
– L. Garde
3 hours ago