Linked Questions

1
vote
1answer
138 views

The existence of unprovably unprovable statements provable in ZFC [duplicate]

I am aware of Gödel's second incompleteness theorem, the proven existence of several unprovable statements (in ZFC), and the possibility that a formal system may include statements that are unprovably ...
2
votes
0answers
41 views

“Nested independence” of $\mathsf{ZFC}$? [duplicate]

I have a question about undecidable statements in $\mathsf{ZFC}$. I know there are true statements like: $$X\text{ is independent of }\mathsf{ZFC}.$$ But is it also possible that such a statement ...
52
votes
3answers
6k views

Is there any conjecture that we know is provable/disprovable but we haven't found a proof of yet?

I know that there are a lot of unsolved conjectures, but it could possible for them to be independent of ZFC (see Could it be that Goldbach conjecture is undecidable? for example). I was wondering if ...
19
votes
4answers
2k views

Is there a statement whose undecidability is undecidable?

We know there are statements that are undecidable/independent of ZFC. Can there be a statement S, such that (ZFC $\not\vdash$ S and ZFC $\not\vdash$ ~S) is undecidable?
11
votes
4answers
1k views

Is every property of the integers provable?

I've been researching provability of properties, and I came across and interesting argument which states that every property of the integers is provable, yet doesn't the incompleteness theorem tell us ...
4
votes
4answers
3k views

How could a statement be true without proof?

Godel`s incompleteness theorem states that there may exist true statements which have no proofs in a formal system of particular axioms. Here I have two questions; 1) How can we say that a statement ...
9
votes
2answers
936 views

In Godel's first incompleteness theorem, what is the appropriate notion of interpretation function?

Wikipedia states Godel's first incompleteness as follows. Any effectively generated theory capable of expressing elementary arithmetic cannot be both consistent and complete. In particular, for any ...
3
votes
2answers
688 views

What would be the consequences if ZFC proved its own inconsistency, nonconstructively? [closed]

Let's say a nonconstructive proof was given in ZFC that ZFC was inconsistent. Note that this doesn't automatically make ZFC inconsistent. Given a consistent theory $X$, $X + \neg \text{Con}(X)$ is ...
10
votes
1answer
483 views

Fixed points in computability and logic

I asked this question on CS.SE, too: https://cstheory.stackexchange.com/questions/27322/fixed-points-in-computability-and-logic I would like to understand better the relation between fixed point ...
2
votes
2answers
135 views

Does ZF $\vdash$ Con(ZF) $\rightarrow$ Con(ZF+$\lnot$AC)?

Certainly ZFC $\vdash$ Con(ZF) $\rightarrow$ Con(ZF+$\lnot$AC), but the usual forcing argument to construct a model of ZF+$\lnot$AC seems to require choice to find a generic filter.
3
votes
1answer
138 views

When can independence of a statement in a theory be reduced to “truth”?

Since the Goldbach conjecture is in $\Pi_1^0$, if it were proven to be independent of Peano Arithmetic, it would follow that the Goldbach conjecture is true (i.e. true in the standard model), since ...
1
vote
1answer
172 views

Legitimacy of Consistency Proofs

In this question I asked yesterday I put forward two interpretations of a statements such as "System X is consistent". (a) we can think of it as saying no finite sequence of applications of logical ...
1
vote
1answer
111 views

On the truth of $GLS$ and Löb's theorem

Consider the formal system $GLS$, whose axioms are the theorems of $GL$ plus all sentences of the form $\square A\rightarrow A$. A translation maps a sentence of modal logic to a sentence in the ...
1
vote
1answer
67 views

primitive recursively axiomatized consistent extension of $PA$. Give sufficient conditions to make statement true

Problem: Let $T$ be a primitive recursively axiomatized consistent extension of $PA$. Under what conditions are each of the following statements true? 1. If $T\vdash\Phi$ then $T\vdash Prov_T([\Phi])...
1
vote
1answer
52 views

Is there a term for this logical property?

Suppose I am working in a standard formal theory such as ZFC or NBG. Consider this statement: "For all well-formed formulas s, ((there exists a proof p s.t. p is a valid proof of s) --> s)" I'm ...