• Starting today August 7th, 2024, in order to post in the Married Couples, Courting Couples, or Singles forums, you will not be allowed to post if you have your Marital status designated as private. Announcements will be made in the respective forums as well but please note that if yours is currently listed as Private, you will need to submit a ticket in the Support Area to have yours changed.

  • CF has always been a site that welcomes people from different backgrounds and beliefs to participate in discussion and even debate. That is the nature of its ministry. In view of recent events emotions are running very high. We need to remind people of some basic principles in debating on this site. We need to be civil when we express differences in opinion. No personal attacks. Avoid you, your statements. Don't characterize an entire political party with comparisons to Fascism or Communism or other extreme movements that committed atrocities. CF is not the place for broad brush or blanket statements about groups and political parties. Put the broad brushes and blankets away when you come to CF, better yet, put them in the incinerator. Debate had no place for them. We need to remember that people that commit acts of violence represent themselves or a small extreme faction.

Mathematical question

GrowingSmaller

Muslm Humanist
Apr 18, 2010
7,424
346
✟56,999.00
Country
United Kingdom
Faith
Humanist
Marital Status
Private
If you'd be willing to say a bit about what motivates your question, that would be good.
Sure. My motive is that I hear about theses and theorems etc in maths that have yet to be proven. There was one asking "is there a highest prime, or do they go on and on?" which I heard about a couple of years ago. Wikipedia has a list of unsolved problems in mathematics. Ordinarily I would think "well, if they can't solve the problem, it's down to not having sufficient mathematical genius." But I also thought, maybe some of there problems and theses etc actually have no solution or proof, because of 'incompleteness' of mathematical systems which Godel demonstrated.

If you want to hear a few of us talk about straight-up mathematical logic and the theory behind Godel's Theorems and formal systems, and go from there, that's cool. I'm sure JonF and I could give it a decent crack.
Ty. I am in awe!:)
 
Upvote 0

Wiccan_Child

Contributor
Mar 21, 2005
19,419
673
Bristol, UK
✟46,731.00
Faith
Atheist
Marital Status
In Relationship
Politics
UK-Liberal-Democrats
Sure. My motive is that I hear about theses and theorems etc in maths that have yet to be proven. There was one asking "is there a highest prime, or do they go on and on?" which I heard about a couple of years ago. Wikipedia has a list of unsolved problems in mathematics. Ordinarily I would think "well, if they can't solve the problem, it's down to not having sufficient mathematical genius." But I also thought, maybe some of there problems and theses etc actually have no solution or proof, because of 'incompleteness' of mathematical systems which Godel demonstrated.
Some of them have proofs which prove there can never be a proof for them :p
 
Upvote 0

Chatter

Newbie
Nov 20, 2010
39
1
✟22,649.00
Faith
Atheist
This is misleading. You can't really have just Goldbach's conjecture as your only axiom. To even formulate Goldbach's conjecture you'd need something like a first (or higher) order logic and ZFC. These necessitate the standard construction of N. So it's possible that Goldbach's conjecture is false in any system it can be stated in.
To formulate Goldbach's conjecture, you just need elementary arithmetic. It sufficies to have a first-order language with equality carrying 0, successor (S), addition (+) and multiplication (*). Primality is then asserted of a variable x with the formula

∀y. (∃z. ¬(z = 0) ∧ y + z = x) ∧ (∃z. y * z = x) → y = S(0))

and Goldbach's conjecture becomes

∀x. (∃y. y + S(S(S(0))) = x) ∧ (∃y. y * S(S(0)) = y) → ∃y z. prime(y) ∧ prime(z) ∧ y + z = x)

There is a consistent theory in the language of arithmetic which has this as its only axiom.

Also Godel's theorem's do apply to inconsistent systems, they actually say a lot about them! Granted, the inconsistent parts of the theorems tend to be largely ignored by non-mathematicians.
Inconsistent systems? There is only one inconsistent system. It is the system which derives every formula, and there isn't much interesting to say about it.

This is not true. For all we know the Goldbach's conjecture is one of the statements described by Godel's incompleteness theorems. If that is the case, it may not be provable in ZFC, but it will be provable in some extension of ZFC. Which is directly related to the question GrowingSmaller asked a few post ago and his question in the OP. Most mathematicians would probably "guess" this isn't the case, because Goldbach's Conjecture is so different than the type of unprovable statement constructed in Godel's Incompleteness Theorems proof. If it's not provable, it's probably axiom independent - which is a completely different equally complicated issue.
No, it cannot be axiom independent in that sense. This is the point I made in my first post, and it is the one thing that Goldbach's conjecture shares with Godel sentences: they are all Π[sub]1[/sub] sentences. If false, they are provably false. You just construct their counterexamples. Thus, if they are undecidable, they must be true.

Goldbach's conjecture is either provably false in theories which embed primitive recursive arithmetic, or it is true, and any such system can add it soundly as an axiom. If it is undecidable, and you add its denial as an axiom, you are no longer sound.
 
Last edited:
Upvote 0

Chatter

Newbie
Nov 20, 2010
39
1
✟22,649.00
Faith
Atheist
Sure. My motive is that I hear about theses and theorems etc in maths that have yet to be proven. There was one asking "is there a highest prime, or do they go on and on?" which I heard about a couple of years ago. Wikipedia has a list of unsolved problems in mathematics. Ordinarily I would think "well, if they can't solve the problem, it's down to not having sufficient mathematical genius." But I also thought, maybe some of there problems and theses etc actually have no solution or proof, because of 'incompleteness' of mathematical systems which Godel demonstrated.
Okay, cool. So the issue of whether there is a highest prime was settled two and a half thousand years ago. A classic and definitive proof is included in Euclid's Elements. If you give me any prime number, no matter how large, I can use it to construct a larger prime in a finite number of steps.

There are certain kinds of unsolved problem that have nothing to do with Godel. For instance, a problem that was outstanding for a few thousand years in classical geometry was to construct a square that has the same area as a circle, but using only ruler and compass. It turned out that the feat was impossible, because the ruler and compass are not sufficiently powerful tools.

Another example of an unsolved problem involves axiom independence. Again, this has little to do with Godel. An example is the problem faced in the centuries following Euclid: how do we derive Euclid's complicated parallel postulate from the other four axioms? It was established in the 19th century that the task is impossible, but not for a lack of tools. The problem was nastier than that, and has been described by historians of mathematics as resulting in a foundational crisis. It was thankfully eliminated when mathematicians relaxed their rigid conception of geometry. This permitted the analysis (some would say discovery) of new kinds of geometry, that have now become the mathematical basis for relativity, and therefore, our understanding of reality itself.

More recently, we have things such as the Continuum Problem. This was an outstanding problem that emerged from set theory, and which a number of analysts were working to solve. It was proved in the mid-20th century (partly by Godel but chiefly by Cohen), that the problem is unsolvable. Again, this is not for a lack of tools, but unlike with Euclid's fifth axiom, we have not found a way to eliminate the problem (so far as I know). The situation is still pretty disturbing.

Now what Godel showed was a bit of tidy mathematical logic: given any formalised axiomatic theory, it is always possible to construct a "problem" that cannot be solved by that theory. However, these problems, or Godel sentences, are not like the malign problems I gave above. Firstly, we are always in a position to assess that Godel sentences are true, even though the axiomatic theories cannot prove them. Secondly, the Godel sentences are not really problems as mathematicians would understand them. They are better described as pathologies, potentially just examples of where our intuitive idea of mathematical theory breaks with the formal idea of an axiomatic theory as studied by mathematical logicians.

The broader question: if we're given a mathematical problem, is there always a way to solve it? Maybe not. As yet, there are no guarantees. The mathematical machinery set up by mathematical logicians to formally ask and answer this question came up with a definitive "no" through Godel. But the "no" answer might just mean "no, mathematical logic cannot answer your question." For as I said, Godel sentences are pretty benign, and Godel's Theorem don't predict the real malign examples such as the Continuum Problem or even Euclid's complex fifth axiom. The real question we want to be asking is: given a mathematical problem that we'd actually care about, such as the outstanding problems in our favourite fields, is there always a way to solve them? Maybe. But don't expect mathematicians to come up with any machinery to answer this question (though you might be amused to know that in my own field, we're trying to get close to it!)
 
Last edited:
Upvote 0

JonF

Sapere Aude!
Site Supporter
Dec 25, 2005
5,094
147
41
California
✟73,547.00
Faith
Calvinist
Marital Status
Married
Politics
US-Republican
To formulate Goldbach's conjecture, you just need elementary arithmetic. It sufficies to have a first-order language with equality carrying 0, successor (S), addition (+) and multiplication (*). Primality is then asserted of a variable x with the formula

[FONT=&quot]∀[/FONT]y. ([FONT=&quot]∃[/FONT]z. ¬(z = 0) [FONT=&quot]∧[/FONT] y + z = x) [FONT=&quot]∧[/FONT] ([FONT=&quot]∃[/FONT]z. y * z = x) → y = S(0))

and Goldbach's conjecture becomes

[FONT=&quot]∀[/FONT]x. ([FONT=&quot]∃[/FONT]y. y + S(S(S(0))) = x) [FONT=&quot]∧[/FONT] ([FONT=&quot]∃[/FONT]y. y * S(S(0)) = y) → [FONT=&quot]∃[/FONT]y z. prime(y) [FONT=&quot]∧[/FONT] prime(z) [FONT=&quot]∧[/FONT] y + z = x)
There is a consistent theory in the language of arithmetic which has this as its only axiom.
If you think those symbols have any meaning without a logic and a theory of sets you are mistaken. If you have a theory of sets and a logic then you are going to have many true statements in your system, and for all you know some of them contradict goldbach’s conjecture. If you choose to use those symbols in their standard way you are assuming ZFC and at least first order logic. If you assume these two, you assume standard N.

Inconsistent systems? There is only one inconsistent system. It is the system which derives every formula, and there isn't much interesting to say about it.
Godel’s incompleteness theorems says a lot about what is sufficient to know a system is inconsistent, and when we can show consistency. Have you read a formal statement of Godel’s Incompleteness Theorems, they say a lot about incompleteness . I mean they very description you just gave of inconsistent systems is a result from Godel's incompleteness theorems.

No, it cannot be axiom independent in that sense. This is the point I made in my first post, and it is the one thing that Goldbach's conjecture shares with Godel sentences: they are all Π[sub]1[/sub] sentences. If false, they are provably false. You just construct their counterexamples. Thus, if they are undecidable, they must be true.
Yes it can, for example if it’s truth was equivalent to the Axiom of choice you wouldn’t be able to construct a counter example to Goldbach’s conjecture for a given number. Or if it’s equivalent to general continuum hypothesis it would be axiom independent. Also, if goldbach's conjecture is false by no means do we need to be able to construct a counter example, it's counter example could exist and not be constructable. Apply what you are claiming to a similar even more primitive concept, "GCH is true unless we can give a counter example", and that is clearly false. If you disagree please give a formal proof that Goldbach’s conjecture is true iff there doesn’t exist a constructable counter example.
 
Last edited:
Upvote 0

Chatter

Newbie
Nov 20, 2010
39
1
✟22,649.00
Faith
Atheist
If you think those symbols have any meaning without a logic and a theory of sets you are mistaken. If you have a theory of sets and a logic then you are going to have many true statements in your system, and for all you know some of them contradict goldbach’s conjecture. If you choose to use those symbols in their standard way you are assuming ZFC and at least first order logic. If you assume these two, you assume standard N.
I'm using those symbols as the signature for a first-order language, and gave an axiom to uniquely define a first-order theory in the resulting language. ZFC is a different first-order theory with its own signature (the single two-place predicate ∈).

At this point, we could get into the question of whether a theory with only that one axiom assigns enough meaning to its signature to really be called a formalisation of a theory which axiomatises the Goldbach conjecture. That's a can of worms I'm happy to broach.

Godel’s incompleteness theorems says a lot about what is sufficient to know a system is inconsistent, and when we can show consistency. Have you read a formal statement of Godel’s Incompleteness Theorems, they say a lot about incompleteness . I mean they very description you just gave of inconsistent systems is a result from Godel's incompleteness theorems.
The fact that there is only one inconsistent system arises from the fact that P ∧ ¬P derives any other formula R in propositional logic, of which first-order theories are extensions. It's not a result of Godel.

Yes it can, for example if it’s truth was equivalent to the Axiom of choice you wouldn’t be able to construct a counter example to Goldbach’s conjecture for a given number. Or if it’s equivalent to general continuum hypothesis it would be axiom independent.
If it is provably equivalent to either, that would be taken as a conclusion that one of AC and CH is false, because arithmetic is Π[sub]1[/sub] sound.

Also, if goldbach's conjecture is false by no means do we need to be able to construct a counter example, it's counter example could exist and not be constructable. Apply what you are claiming to a similar even more primitive concept, "GCH is true unless we can give a counter example", and that is clearly false. If you disagree please give a formal proof that Goldbach’s conjecture is true iff there doesn’t exist a constructable counter example.
You're asking me to prove that arithmetic is Π[sub]1[/sub] sound :p? It can be done. I have a fully machine verified proof of it on my computer, though it isn't very enlightening. If you think that the soundness of arithmetic needs proving, you certainly have my respect, but it means shying away from the colloquial descriptions of Godel's Theorem: accordingly, Godel didn't prove that there are true but unprovable statements in any theory. He just proved that there are unprovable statements on the assumption of a system's consistency.
 
Last edited:
Upvote 0

JonF

Sapere Aude!
Site Supporter
Dec 25, 2005
5,094
147
41
California
✟73,547.00
Faith
Calvinist
Marital Status
Married
Politics
US-Republican
Oh man, you’re gonna make me go find and dust of my book on Godel’s incompleteness theorems aren’t you?
I'm using those symbols as the signature for a first-order language, and gave an axiom to uniquely define a first-order theory in the resulting language. ZFC is a different first-order theory with its own signature (the single two-place predicate
∈).

At this point, we could get into the question of whether a theory with only that one axiom assigns enough meaning to its signature to really be called a formalisation of a theory which axiomatises the Goldbach conjecture. That's a can of worms I'm happy to broach.
Your "single axiom" system uses conjunction, quantifiers, negation. You may only state one axiom, but you have all of the axioms of some set theory and some f.o.l. hidden in there too. You may be using an a-typical water downed system, like BA or Q but even then you still are using a water down logic and set theory with all of it's axioms. You would still run into consistency problems with Goldbach conjecture if it is false in Q if you took it as an axiom pretty much anywhere.

If it is provably equivalent to either, that would be taken as a conclusion that one of AC and CH is false, because arithmetic is Π[sub]1[/sub]
I understand arithmetic is Π1 sound. This only means for any Arithmetic system A and p a Π-sentence (which I agree goldbach’s conjecture is one) then if A |- p then p is true. You are reversing the direction of the last inference. What you are describing is Π-complete, which isn’t true for any arithmetic systems. Granted Q is
∑1 complete (I think any of its extensions aren’t though I if I remember correctly? I could be wrong on this). So I guess if Goldbach’s conjecture was false then its negation would be a true ∑1 sentence, so it would be provable. But that doesn’t really comment on axiom independence. Since if it were axiom independent the supposition that it is false in Q would also be false.

You're asking me to prove that arithmetic is Π[sub]1[/sub] sound
clip_image001.gif
? It can be done. I have a fully machine verified proof of it on my computer, though it isn't very enlightening. If you think that the soundness of arithmetic needs proving, you certainly have my respect, but it means shying away from the colloquial descriptions of Godel's Theorem: accordingly, Godel didn't prove that there are true but unprovable statements in any theory. He just proved that there are unprovable statements on the assumption of a system's consistency.
I know arithmetic (in Q) is Π[sub]1[/sub] sound, I also know that arithmetic is not is Π [sub]1[/sub] complete.
 
Upvote 0

Chatter

Newbie
Nov 20, 2010
39
1
✟22,649.00
Faith
Atheist
Your "single axiom" system uses conjunction, quantifiers, negation. You may only state one axiom, but you have all of the axioms of some set theory and some f.o.l. hidden in there too. You may be using an a-typical water downed system, like BA or Q but even then you still are using a water down logic and set theory with all of it's axioms. You would still run into consistency problems with Goldbach conjecture if it is false in Q if you took it as an axiom pretty much anywhere.
I am assuming the whole of FOL, since I am talking about a first-order theory with that axiom. There's no consistency problems. The formalisation I gave is true for the trivial interpretation with one object, so the first-order theory which has it as its sole axiom is consistent.

I'm not sure why you keep mentioning set-theory. Set theory is a specific first-order theory. First-order theories are not generally extensions of any set theory.

I understand arithmetic is Π1 sound. This only means for any Arithmetic system A and p a Π-sentence (which I agree goldbach’s conjecture is one) then if A |- p then p is true. You are reversing the direction of the last inference. What you are describing is Π-complete, which isn’t true for any arithmetic systems. Granted Q is
∑1 complete (I think any of its extensions aren’t though I if I remember correctly? I could be wrong on this). So I guess if Goldbach’s conjecture was false then its negation would be a true ∑1 sentence, so it would be provable. But that doesn’t really comment on axiom independence. Since if it were axiom independent the supposition that it is false in Q would also be false.
Yes, I got "soundness" and "completeness" badly muddled there :doh:. But the point you make here is exactly what I said earlier: if Goldbach's conjecture is false, it is provably false. This does affect axiom independence. It means that if Goldbach's conjecture is independent of Q, or PA, or ZFC, then it must be true, and any system which has it as an axiom is a system which is unsound, since it contains non-standard numbers, exactly as what happens when you add the negations of Godel sentences as axioms.
 
Upvote 0

liars_paradox

Senior Member
Jun 8, 2009
788
38
North Carolina
✟24,505.00
Country
United States
Gender
Male
Faith
Protestant
Marital Status
Single
Politics
US-Republican
IIRC Godel's incompleteness theorem says something like in a formal system of maths there are some statements which cannot be proven to be true or false within that system. What I want to know is could Goldbach's conjecture be one such statement.

Does this really belong in Philosophy? This sounds more like computer science theory rather than philosophy!
 
Upvote 0

Eudaimonist

I believe in life before death!
Jan 1, 2003
27,482
2,738
58
American resident of Sweden
Visit site
✟126,756.00
Gender
Male
Faith
Atheist
Marital Status
Private
Politics
US-Libertarian
Does this really belong in Philosophy? This sounds more like computer science theory rather than philosophy!

Logic pertains to philosophy, and computer science and mathematics are applications of logic.

Yes, it's philosophy, albeit an "applied" philosophy.


eudaimonia,

Mark
 
Upvote 0

JonF

Sapere Aude!
Site Supporter
Dec 25, 2005
5,094
147
41
California
✟73,547.00
Faith
Calvinist
Marital Status
Married
Politics
US-Republican
[FONT=&quot]I am assuming the whole of FOL, since I am talking about a first-order theory with that axiom. There's no consistency problems. The formalisation I gave is true for the trivial interpretation with one object, so the first-order theory which has it as its sole axiom is consistent. [/FONT]
[FONT=&quot]My point is that you need to assume some logic (you assume FOL) and some set theory (doesn’t have to be ZFC, but quantifiers require sets to some degree) to even formulate something like Goldbach’s conjecture. Otherwise it’s just a meaningless pattern of symbols. In assuming this set theory and logic you are inadvertently adding all of the axioms of that logic and set theory to your system. Your claim was you can have a system where Goldbach’s conjecture is the only axiom. Well sure I guess you could, but the symbols in the conjecture would have no meaning then.[/FONT]
[FONT=&quot]
I'm not sure why you keep mentioning set-theory. Set theory is a specific first-order theory. First-order theories are not generally extensions of any set theory.
I keep saying set theory because I’m try not to bottle neck you into ZFC or any particular axiomatic approach to sets. But basically your theory needs to describe sets to formulate Goldbach’s Conjecture.

Yes, I got "soundness" and "completeness" badly muddled there
[/FONT]
clip_image001.gif
[FONT=&quot]. But the point you make here is exactly what I said earlier: if Goldbach's conjecture is false, it is provably false. This does affect axiom independence. It means that if Goldbach's conjecture is independent of Q, or PA, or ZFC, then it must be true, and any system which has it as an axiom is a system which is unsound, since it contains non-standard numbers, exactly as what happens when you add the negations of Godel sentences as axioms.[/FONT]
Underlined is what i disagree with and i don't think you've shown it.

Yes, it's philosophy, albeit an "applied" philosophy.
Ack, did you just call pure math applied philosophy? I think you made me cry on the inside :(.
 
Last edited:
Upvote 0

Eudaimonist

I believe in life before death!
Jan 1, 2003
27,482
2,738
58
American resident of Sweden
Visit site
✟126,756.00
Gender
Male
Faith
Atheist
Marital Status
Private
Politics
US-Libertarian
  • Like
Reactions: JonF
Upvote 0

Chatter

Newbie
Nov 20, 2010
39
1
✟22,649.00
Faith
Atheist
[FONT=&quot]My point is that you need to assume some logic (you assume FOL) and some set theory (doesn’t have to be ZFC, but quantifiers require sets to some degree) to even formulate something like Goldbach’s conjecture. Otherwise it’s just a meaningless pattern of symbols. In assuming this set theory and logic you are inadvertently adding all of the axioms of that logic and set theory to your system. Your claim was you can have a system where Goldbach’s conjecture is the only axiom. Well sure I guess you could, but the symbols in the conjecture would have no meaning then.[/FONT]
Why does the addition of the axioms of ZFC suddenly give such a formula meaning? The way you are using the word "meaning" doesn't look very precise to me. There are plenty of ways to talk about the meaning of formulas in mathematical logic. We can talk about formal semantics, standard models of natural numbers, and in the case of arithmetic, representability.

There is a precise sense in which the formula I gave is Goldbach's conjecture: Goldbach's conjecture is true exactly when the formula I gave is true of the standard interpretation of natural numbers in the first-order language of arithmetic.
[FONT=&quot]
[/FONT]
Underlined is what i disagree with and i don't think you've shown it.
You agreed earlier that Q is Σ[sub]1[/sub] complete. The denial of Goldbach's conjecture is Σ[sub]1[/sub]. So if Goldbach's conjecture is false (its denial is true), then it is provably false in Q. Thus, if Q doesn't decide Goldbach's conjecture, then it doesn't, in particular, prove Goldbach's conjecture false, and so it must be true.

That was more complicated than it needed to be. Here's another way to put it: given a natural number, there is an effective procedure to determine whether that natural number is an even number greater than 2 and whether it is the sum of two primes. According to the representability theorems, that means that in an enumeration of all the theorems of Q, every single natural number will eventually be tested to see if it is an even number greater than 2 and the sum of two primes. If Goldbach's conjecture is false, it's refutation must appear in that enumeration. If the refutation does not appear because Goldbach's conjecture is undecidable in Q, then it cannot be false.

Ack, did you just call pure math applied philosophy? I think you made me cry on the inside :(.
And I just feel dirty. At best, it's the philosophers who apply the maths (and usually badly :p )
 
Upvote 0

GrowingSmaller

Muslm Humanist
Apr 18, 2010
7,424
346
✟56,999.00
Country
United Kingdom
Faith
Humanist
Marital Status
Private
Chatter said:
That was more complicated than it needed to be. Here's another way to put it: given a natural number, there is an effective procedure to determine whether that natural number is an even number greater than 2 and whether it is the sum of two primes.
It can't be that effective, if it hasn't answered the question yet, or can it (or has it)? Are we talking about an infinite series of steps in the "effective" procedure.

"Take these. In 23 trillion lifetimes you won't be feeling any better at all.":D
 
Upvote 0

Chatter

Newbie
Nov 20, 2010
39
1
✟22,649.00
Faith
Atheist
It can't be that effective, if it hasn't answered the question yet, or can it (or has it)? Are we talking about an infinite series of steps in the "effective" procedure.
It's a technical term. Here, I just mean you could get a computer to do it. But we're not talking about getting a computer to figure out the Goldbach conjecture. We're just talking about whether a computer program can test whether its input is a counterexample of the Goldbach conjecture. It can always do this in a reasonable and finite amount of time. It would obviously take you forever to run that algorithm over all integers.
 
Upvote 0

GrowingSmaller

Muslm Humanist
Apr 18, 2010
7,424
346
✟56,999.00
Country
United Kingdom
Faith
Humanist
Marital Status
Private
It's a technical term.
I know, just fooling around, soz.
It would obviously take you forever to run that algorithm over all integers.
Which is what would be required
for a proof that the GC is true, right?:cool: Or wrong?:doh:
 
Upvote 0

Chatter

Newbie
Nov 20, 2010
39
1
✟22,649.00
Faith
Atheist
I know, just fooling around, soz.Which is what would be required
for a proof that the GC is true, right?:cool: Or wrong?:doh:
Not quite right. But this nicely takes us back to your original question.

If GC is just completely unprovable, then you can't do better than checking through all integers and imagining that you could somehow see to the end of this possibly infinite process. You could see that far ahead if you had an oracle, a kind of hypercomputer, which solves the halting problem, seeing whether or not the counterexample finder succeeds in its goal or fails and runs forever.

But if GC is provable in an appropriate formal system, then you can just enumerate all the theorems of that formal system (by definition, this enumeration must be effective), looking for the statement of the Goldbach conjecture. It would take only finite time.
 
Upvote 0