Prove I’mUnprovable using proof by contradictions as follows:
In order to obtain a contradiction, hypothesize
¬I’mUnprovable. Therefore ⊢I’mUnprovable
(using I’mUnprovable⇔⊬I’mUnprovable). Consequently,
⊢⊢I’mUnprovable using ByProvabilityOfProofs
{⊢∀[Ψ:Proposition<i>] (⊢Ψ)⇒⊢⊢Ψ}. However,
⊢¬I’mUnprovable (using I’mUnprovable ⇔⊬I’mUnprovable),
which is the desired contradiction in foundations.
Consequently, I’mUnprovable has been proved to be
a theorem using proof by contradiction in which
¬I’mUnprovable is hypothesized and a contradiction derived.
In your notation, the proof shows that following holds:
¬I’mUnprovable ⇒ ⊥
Why do you think that the proof is for the following?
Edit: if you had as an axiom, or could otherwise prove within the system, that ¬◻⊥, I.e. that the system is consistent, then you could conclude from ◻P and ◻¬P that ⊥, by first concluding ◻⊥, and then combining this with ¬◻⊥ .
And in this case, you could indeed say that this is a contradiction, and therefore reject the assumption of ¬UNK, and then conclude UNK without assumptions.
So, if one could show ¬◻⊥ (or if the system had it as an axiom), the reasoning would go through. (This is the thing that is missing.)
Therefore, you could then prove ◻UNK, and therefore ¬UNK, and therefore (having already shown UNK) would have a contradiction, ⊥.
So, this is a way of showing that, if you can show ¬◻⊥ (and if there is a statement UNK), then the system is inconsistent. Which is just one of Gödel’s theorems: a strong system can’t prove its own consistency without being inconsistent.
By the way, because the proposition I'mUnprovable does not
exist in foundations, it is OK for foundations to prove
their own consistency as follows:
Consistency of a theory can be formally defined as follows:
Consistent⇔¬∃[Ψ] ⊢Ψ∧¬Ψ
Contra [Gödel 1931], a foundational theory can prove its own
consistency as shown in the following theorem:
Classical theorem. ⊢Consistent
Classical proof. In order to obtain a contraction,
hypothesize ¬Consistent. Consequently,
¬¬∃[Ψ] ⊢Ψ∧¬Ψ, which classically implies ∃[Ψ]⊢Ψ∧¬Ψ by
double negation elimination. Consequently, there is a
proposition Ψ0 such that ⊢Ψ0∧¬Ψ0 (by eliminating the
existential quantifier in ∃[Ψ]⊢Ψ∧¬Ψ). By the principle
of ByTheoremUse {⊢∀[Φ] (⊢Φ)⇒Φ} with Ψ0 for Φ, Ψ0∧¬Ψ0,
which is the desired contradiction.
However, the proof does not carry conviction that a
contradiction cannot be derived because the proof is valid
even if the theory is inconsistent. Consistency of the
mathematical theories Actors and Ordinals is established by
proving each theory has a unique-up-to-isomorphism model
ByTheoremUse is not a valid principle, at least for any system that includes Peano Arithmetic.
(It is essentially the assumption that the system is not only consistent, but sound. It is therefore no surprise that ByTheoremUse would imply Consistent.)
By Löb’s theorem, ByTheoremUse would imply that for all propositions P, that P holds. I.e. it implies ⊥.
Perhaps I misunderstood what you mean by ByTheoremUse .
If you mean that, if in a context/environment with certain givens, one can derive a conclusion, then one can apply that in other cases,
Or if you just mean modus ponens, or cut elimination,
Then ok, that’s fine. That’s valid. (Though it doesn’t justify the step you cited it in.)
But you can’t, within the system, go from ◻P to P. That isn’t a valid rule of inference.
There’s a distinction between “therefore P” and “therefore ◻P”, and you cannot use the latter as the former.
You seem to equivocate better “P is provable” and “therefore P”
Like, suppose I was writing a computer program in a strongly typed language, and something required an argument of type A->B , and I tried to pass in a string which has the text of a function with that type. Obviously that wouldn’t type check.
I don't know that I can derive it in the system you described which you are calling "foundations", because I'm not sure that it is sufficiently clearly defined to, uh, clearly express a particular formal system.
In other systems, yes, I can prove a contradiction using ByTheoremUse . Because of Lob's theorem (which I can prove).
(examples of issues in the descriptions you give of the system you attempt to define:
After introducing the standard notation that x:T is to be interpreted as x is of type T, you later go on to talk about "x:Term<T>" for some type T. What this is supposed to mean is very unclear. If what you mean by it is "x is a term of type T", then, in the ordinary sense, this would be the same thing as saying x:T . But if this is all you meant, presumably you would have just written that. So it seems that you mean to have that there are some cases where "x is of type T" and "x is a term of type T" mean different things. In this case, you should clarify what you are using "term" to mean, because it does not seem to be the usual use of the term.
You also say x2^{x1}:Term<t2^{t1}> , when t2^{t1} has been defined to be the type of functions from the type t1 to the type t2.
What in the world is this supposed to be? Given a term of type t1 and a term of type t2, what function from t1 to t2 is this supposed to represent? The only one which this would guarantee to exist would be the constant function that sends everything to the given term of type t2 (so, sends everything to x2). But in this case, why require a term of type t1? The only point to that that I can see, would be to guarantee that the type t1 is nonempty, if for some reason you didn't want to allow functions with empty domain. What is the purpose of this?
In your system which is intended to be a foundation of things, you seem to implicitly assume that there is some parameterized type called 1to1, which you don't define. Now, presumably you mean for this to be the type of bijections from the type/set which is the first argument to the type/set which is the second argument, and of course such a thing should exist, but, seeing as you are laying out an attempt at a foundational system, you really ought to actually define it. Either it should be given a definition within the system, or, if it is meant to be an irreducible part of the system, the rules of inference around it should be given.
You do the same thing with "TermWithNoFreeVariables". This is mixing up different levels of description.
You never describe what String<TermWithNoFreeVariables<t>> is supposed to mean.
If the text colors you gave to parts of it was supposed to mean anything, you don't say what it is that the colors mean. As is, they are simply distracting.
You also assert that in constructive type theory uses the assumption that something is a proposition of a theory only if it is a theorem of the theory? This is false. It is difficult to understand the confusion which would lead to such a conclusion. You also assert that constructive type theories have, instead of a type of all functions from t_1 to t_2, instead have a type of computable functions from t_1 to t_2. There are a couple things you could have meant by this, but the interpretation that seems probably the most straightforwards interpretation is false I think? Just because you can't construct a function doesn't mean that it isn't in the function type in question, and anything which accepts that function type as an argument, must be able to handle any such function. Well, this may depend somewhat on the specific system in use, but in all the ones I've dealt with, this doesn't seem to apply.
You also assert that theorems in your system are not computationally enumerable due to (something) being uncountable, and that simultaneously proof checking is decidable in your system. This is obviously false.
If proof checking is decidable for a given system, then there is a computational procedure which, for any finite string of text, will decide within finite time whether it is a valid proof within the system. (This is what it means for proof checking to be decidable.)
The set of finite strings (over a given alphabet) is computationally enumerable. Obviously.
Simply iterate over the finite strings, and for each of them, run the procedure to evaluate whether it is a valid proof.
This obviously produces an enumeration of all valid proofs of the system.
Unless, perhaps, you are saying that there is no decidable procedure which, given a valid proof, determines the statement that it is a proof of? If so, that would be stupid.
I suppose if I define some countable set which is not computationally enumerable, and call the elements of that set "theorems", and then define some uncomputable surjective function from the integers to this set, and call the integers "proofs", then I could say that for each "theorem" there is a proof, and that deciding whether an input integer is a valid proof is decidable (as the answer would always be yes), but that the theorems aren't computationally enumerable, but that would be stupid.
A formal system can, of course, have uncountable models. (Well, modulo metaphysical disputes)
But you talk about having "uncountable proof checkers" because of proof checkers not being restricted to strings?
Among an uncountable set, not all elements of it can be named using any finite name.
The set of possible inputs to a computer for which the computer halts within finite time, up to considering equivalent those inputs which only differ in parts that computer does not check/is-not-influenced-by, is countable.
Or, if you want to appeal to supertask style hypercomputation, you should say so explicitly, probably in the abstract.
If something isn't representable as a string, I would say it isn't a proof, at least in the default sense of the term.
a theorem using proof by contradiction in which
¬I’mUnprovable is hypothesized and a contradiction derived.
In your notation, the proof shows that following holds:
Why do you think that the proof is for the following?