[FOM] Untyped/typed and bivalent/multivalent

[Patrik Eklund]

An intuitive, but very fundamental question:

If set theory is untyped (at least in some sense) and bivalent, how can 
it be a foundation for something typed and something multivalent?

Take, for instance, Kleene's three-valued logic, used in context of 
recursion and related to treatment of partial mappings. The conjunction 
is commutative, but I wonder how we can justify it. It may one such 
"wisdom" (Harvey's recent posting), and simply "brought in" from the 
outside. This is then multivalent, and a non-commutative (tensored) 
conjunction is also possible. A justification obviously cannot reside 
within ZFC, but at the same time that choice affects recursion, and 
would require to check a number of things. Bocvar called that in-between 
value "senseless", whereas Kleene called it "unspecified".

The foundations of set theory and logic were developed hand-in-hand and 
is "intertwined". Type theory tries to do it "all-in-one", or actually 
using logic without set theory. Problems arise with type constructors, 
and the way types are manipulated using entailment is not all that 
convincing. It mixes bags, so as to say.

---

On 2016-03-30 23:20, Harvey Friedman wrote:
...
> a. A framework for doing some new kinds of abstract categorical
> algebra/topology that is exciting to very abstractly minded
> mathematicians.
> b. A complicated solution in search of a foundational problem.
> 
> So I repeat my suspicion and therefore my challenge.

---

I would say it's neither categorical algebra nor topological. It makes 
analogy with homotopy, and even tries to provide an abstraction of 
homotopy. TT now knows it needs categorical constructions, but it still 
does not deal properly with type constructors.

Harvey sees no semantics, and neither do I. In TT, saying "propositions 
are types" is very close to saying "sets are types". However, TT can 
avoid doing that because they never expose the distinction between 
syntactic proposition and semantic proposition. Note that in programming 
languages there is a similar confusion. If we declare "x : nat" we say 
we have a syntactic form of a variable of type nat, but when we do "x = 
0" we are in fact making an assignment, not a substitution!, so "x" in 
"X = 0" is then the semantic counterpart of the syntactic "x" in "x : 
nat". Computer scientists don't care, because their (our, I should say, 
since I'm a professor in computer science) ego is larger than that. 
"Propositions are types" are generalized to "proofs as programs", so CS 
believes "algorithm = FOM".

Within category there has been a number of debates thought decades about 
CT as a foundation itself. The general view, however, is still that ZFC 
is the meta-foundation for CT, and my conviction is that, given this 
circumstance, TT's issue about type constructors can be treated within 
CT, so my claim is simple:

Type foundations can be treated within CT, with ZFC as its foundation. 
Or to make it even simpler. In set theory, there is no debate about the 
empty set. In type theory, the "empty type" is tricky.

I look forward to comments.

Patrik