Return to Answer

The statement in question can be formalized in the language of Peano Arithmetic, and I will treat it as a statement in that language. A similar analysis works for any effective theory stronger than PA, such as ZFC.

Consider the set of all sentences in the language of PA; define an order relation $R$ so that $\phi \mathbin{R} \psi$ if $\phi \to \psi$ is provable in PA. This gives a pre-order; if we perform the usual equivalence class construction then the resulting algebra is a partial order called a Lindenbaum algebra (*).

Because the graph reconstruction conjecture corresponds to a sentence $G$ in PA, it corresponds to a particular node in this algebra.

• If $G$ is provable in PA, then $G$ corresponds to the bottom element of the algebra
• If $G$ is false, it corresponds to the top node of the algebra, but in this case we're not very worried about its provability
• Otherwise, $G$ corresponds to some intermediate node of the algebra. In that case, we cannot prove $G$ from PA, but we can prove $G$ by assuming PA plus any axiom either in the equivalence class of sentences that forms $G$'s node or in the equivalence class of any node higher than $G$'s node.

In every case, unless $G$ is false, $G$ is amenable to proof, but the proof will have to assume axioms that are strong enough to prove the desired conclusion. There is no sentence which could "never actually be proved", although there are plenty of sentences that cannot be proved in PA, and false sentences can only be proved from false axioms. The question is simply which axioms are required to prove a particular sentence.

*: Traditionally, a "Lindenbaum algebra" or "Lindenbaum–Tarski algebra" should be defined with the dual ordering of the ordering I use. But the ordering in which $0=1$ corresponds to the top of the algebra matches better with the diagrams we create to illustrate relationships between different axiom systems, such as 1. People also use the reverse ordering in the context of set theory, where large cardinal axioms are sorted by consistency strength, e.g. 2.

The statement in question can be formalized in the language of Peano Arithmetic, and I will treat it as a statement in that language. A similar analysis works for any effective theory stronger than PA, such as ZFC.

Consider the set of all sentences in the language of PA; define an order relation $R$ so that $\phi \mathbin{R} \psi$ if $\phi \to \psi$ is provable in PA. This gives a pre-order; if we perform the usual equivalence class construction then the resulting algebra is a partial order called a Lindenbaum algebra (*).

Because the graph reconstruction conjecture corresponds to a sentence $G$ in PA, it corresponds to a particular node in this algebra.

• If $G$ is provable in PA, then $G$ corresponds to the bottom element of the algebra
• If $G$ is false, it corresponds to the top node of the algebra, but in this case we're not very worried about its provability
• Otherwise, $G$ corresponds to some intermediate node of the algebra. In that case, we cannot prove $G$ from PA, but we can prove $G$ by assuming PA plus any axiom either in the equivalence class of sentences that forms $G$'s node or in the equivalence class of any node higher than $G$'s node.

In every case, unless $G$ is false, $G$ is amenable to proof, but the proof will have to assume axioms that are strong enough to prove the desired conclusion. There is no sentence which could "never actually be proved", although there are plenty of sentences that cannot be proved in PA, and false sentences can only be proved from false axioms. The question is simply which axioms are required to prove a particular sentence.

*: Traditionally, a "Lindenbaum algebra" or "Lindenbaum–Tarski algebra" should be defined with the dual ordering of the ordering I use. But the ordering in which $0=1$ corresponds to the top of the algebra matches better with the diagrams we create to illustrate relationships between different axiom systems, such as 1. People also use the reverse ordering in the context of set theory, where large cardinal axioms are sorted by consistency strength, e.g. 2.

The statement in question can be formalized in the language of Peano Arithmetic, and I will treat it as a statement in that language. A similar analysis works for any effective theory stronger than PA, such as ZFC.

Consider the set of all sentences in the language of PA; define an order relation $R$ so that $\phi \mathbin{R} \psi$ if $\phi \to \psi$ is provable in PA. This gives a pre-order; if we perform the usual equivalence class construction then the resulting algebra is a partial order called a Lindenbaum algebra (*).

Because the graph reconstruction conjecture corresponds to a sentence $G$ in PA, it corresponds to a particular node in this algebra.

• If $G$ is provable in PA, then $G$ corresponds to the bottom element of the algebra
• If $G$ is false, it corresponds to the top node of the algebra, but in this case we're not very worried about its provability
• Otherwise, $G$ corresponds to some intermediate node of the algebra. In that case, we cannot prove $G$ from PA, but we can prove $G$ by assuming PA plus any axiom either in the equivalence class of sentences that forms $G$'s node or in the equivalence class of any node higher than $G$'s node.

In every case, unless $G$ is false, $G$ is amenable to proof, but the proof will have to assume axioms that are strong enough to prove the desired conclusion. There is no sentence which could "never actually be proved", although there are plenty of sentences that cannot be proved in PA, and false sentences can only be proved from false axioms. The question is simply which axioms are required to prove a particular sentence.

*: Traditionally, a "Lindenbaum algebra" or "Lindenbaum–Tarski algebra" should be defined with the dual ordering of the ordering I use. But the ordering in which $0=1$ corresponds to the top of the algebra matches better with the diagrams we create to illustrate relationships between different axiom systems, such as 1 and 2.

The statement in question can be formalized in the language of Peano Arithmetic, and I will treat it as a statement in that language. A similar analysis works for any effective theory stronger than PA, such as ZFC.

Consider the set of all sentences in the language of PA; define an order relation $R$ so that $\phi \mathbin{R} \psi$ if $\phi \to \psi$ is provable in PA. This gives a pre-order; if we perform the usual equivalence class construction then the resulting algebra is a partial order called a Lindenbaum algebra (*).

Because the graph reconstruction conjecture corresponds to a sentence $G$ in PA, it corresponds to a particular node in this algebra.

• If $G$ is provable in PA, then $G$ corresponds to the bottom element of the algebra
• If $G$ is false, it corresponds to the top node of the algebra, but in this case we're not very worried about its provability
• Otherwise, $G$ corresponds to some intermediate node of the algebra. In that case, we cannot prove $G$ from PA, but we can prove $G$ by assuming PA plus any axiom either in the equivalence class of sentences that forms $G$'s node or in the equivalence class of any node higher than $G$'s node.

In every case, unless $G$ is false, $G$ is amenable to proof, but the proof will have to assume axioms that are strong enough to prove the desired conclusion. There is no sentence which could "never actually be proved", although there are plenty of sentences that cannot be proved in PA, and false sentences can only be proved from false axioms. The question is simply which axioms are required to prove a particular sentence.

*: Traditionally, a "Lindenbaum algebra" or "Lindenbaum–Tarski algebra" should be defined with the dual ordering of the ordering I use. But the ordering in which $0=1$ corresponds to the top of the algebra matches better with the diagrams we create to illustrate relationships between different axiom systems, such as 1. People also use the reverse ordering in the context of set theory, where large cardinal axioms are sorted by consistency strength, e.g. 2.

The statement in question can be formalized in the language of Peano Arithmetic, and I will treat it as a statement in that language. A similar analysis works for any effective theory stronger than PA, such as ZFC.

Consider the set of all sentences in the language of PA; define an order relation $R$ so that $\phi \mathbin{R} \psi$ if $\phi \to \psi$ is provable in PA. This gives a pre-order; if we perform the usual equivalence class construction then the resulting algebra is a partial order called a Lindenbaum algebra.

Because the graph reconstruction conjecture corresponds to a sentence $G$ in PA, it corresponds to a particular node in this algebra.

• If $G$ is provable in PA, then $G$ corresponds to the bottom element of the algebra
• If $G$ is false, it corresponds to the top node of the algebra, but in this case we're not very worried about its provability
• Otherwise, $G$ corresponds to some intermediate node of the algebra. In that case, we cannot prove $G$ from PA, but we can prove $G$ by assuming PA plus any axiom either in the equivalence class of sentences that forms $G$'s node or in the equivalence class of any node higher than $G$'s node.

In every case, unless $G$ is false, $G$ is amenable to proof, but the proof will have to assume axioms that are strong enough to prove the desired conclusion. There is no sentence which could "never actually be proved", although there are plenty of sentences that cannot be proved in PA, and false sentences can only be proved from false axioms. The question is simply which axioms are required to prove a particular sentence.

The statement in question can be formalized in the language of Peano Arithmetic, and I will treat it as a statement in that language. A similar analysis works for any effective theory stronger than PA, such as ZFC.

Consider the set of all sentences in the language of PA; define an order relation $R$ so that $\phi \mathbin{R} \psi$ if $\phi \to \psi$ is provable in PA. This gives a pre-order; if we perform the usual equivalence class construction then the resulting algebra is a partial order called a Lindenbaum algebra (*).

Because the graph reconstruction conjecture corresponds to a sentence $G$ in PA, it corresponds to a particular node in this algebra.

• If $G$ is provable in PA, then $G$ corresponds to the bottom element of the algebra
• If $G$ is false, it corresponds to the top node of the algebra, but in this case we're not very worried about its provability
• Otherwise, $G$ corresponds to some intermediate node of the algebra. In that case, we cannot prove $G$ from PA, but we can prove $G$ by assuming PA plus any axiom either in the equivalence class of sentences that forms $G$'s node or in the equivalence class of any node higher than $G$'s node.

In every case, unless $G$ is false, $G$ is amenable to proof, but the proof will have to assume axioms that are strong enough to prove the desired conclusion. There is no sentence which could "never actually be proved", although there are plenty of sentences that cannot be proved in PA, and false sentences can only be proved from false axioms. The question is simply which axioms are required to prove a particular sentence.

*: Traditionally, a "Lindenbaum algebra" or "Lindenbaum–Tarski algebra" should be defined with the dual ordering of the ordering I use. But the ordering in which $0=1$ corresponds to the top of the algebra matches better with the diagrams we create to illustrate relationships between different axiom systems, such as 1 and 2.