By the way, your posts are coming out formatted in a way that makes them fairly hard to read...

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.