[FOM] Untyped/typed and bivalent/multivalent
Patrik Eklund
peklund at cs.umu.se
Thu Mar 31 03:02:14 EDT 2016
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
More information about the FOM
mailing list