Lambda the Ultimate

What does "Types categorically axiomatise uncountably many Reals" mean? I understand types, categories, axioms, uncountable things and what a real number is, yet that sentence means nothing to me.

You cannot realise uncountably many Reals, categorically or otherwise. The human brain with a finite number if neurons cannot contain infinite anything. The universe with finite qbits cannot contain infinite anything. Realising an infinity of anything is impossible. You can axiomatically describe the infinity using the Peano/Dedekind axioms, and that is how the human brain reasons about them. You reason about Pi by approximating the value or series expansion.

What we have here I think is a classic philosophical category error. Referencing Wittgenstein, we have one language game for countable things, things that exist, like how many stones in this pile. We then have an abstract language game, based on induction, where we say: "the sun has come up every morning so far, therefore we expect that it comes up every morning forever". Despite the fact that this is not true, we can imagine a universe in which it is true. What we have is concrete observed reality, and an abstract fantasy. Now we find we can reason about infinities and come up with sensible results (second order logic), and we know we can still count finite sets (first order logic). We even share words between the language games such that we might have a first order concept of addition, and a second order concept of addition. The mistake is to try and make those two concepts of additions the same. They share the same name because they seem to do similar things in both language games, but they are not the same thing. By trying to make them the same thing you introduce an error in that you can now say you have uncountably many countable things.

You can define an interpreter for second order logic in first order logic, and I think this is how the human brain reasons about second order things, after all the brain is constructed from a finite number of neurons. In this case the rules and conclusion about second order addition clearly do not apply to the host (first order system).

What does "Types categorically axiomatise uncountably many Reals" mean? I understand types, categories...

Don't forget that "categorical" is a concept in model theory and is not especially related to "categories."

Okay, so it means one model up to isomorphism. This seems irrelevant to realisability, and does not change my reasoning above.

I disagree that the constructable Reals are uncountable. As we can Godel number any generator function of Real numbers (in the same way we can count using Natural numbers). Constructable has to take into account finite time and memory. You cannot construct uncountably many Real numbers in this universe.

I can construct a sentence that talks about uncountable Reals, but that sentence does not actually contain all the Reals. This is simply a statement in second order logic, and all statements in second order logic (that you can write down) have a finite Gödel number.

The constructable reals are countable.

They are uncomputably countable.

Go figure.

Types mean that "I am not provable" is not a sentence of Mathematics.

However, types must be powerful enough that all of Mathematics can be done using types.

Clearly the Godel number corresponds to the neuron numbering in the network. The human brain has a finite number of neurons (hence all Godel numbers assigned are finite) yet we can understand and reason about real numbers. Effectively any real number you can imagine has a finite Godel number. Hence sentences and propositions are countable because the representation of them in the network is finite. Literally anything you can think or reason about has a finite Godel number.Conversely the human brain cannot reason or even imagine anything with a non-finite Godel number. Hence your system must have finite Godel numbers as you can reason about it using a finite number of neurons.

Direct Logic is intended to be a rigorous mathematical foundation for Computer Science. However, it is still relatively new and consequently may have some bugs although it has been presented and reviewed by world-class experts during its development. Thomas has presented an excellent overview in his post above :-) The current published articles on Direct Logic are designed for readers who are already experts. It would be very helpful to have articles for other audiences.

Of course, there is still much work to be done including some open issues to be addressed.

The core of CDL is deliberately ambigous in an unusual way. It is not simply that there are multiple possible models of CDL. The ambiguity is deeper than that. There is no model for CDL -- only for CDL plus additional axioms (which we could call the "sub-theories" of CDL).

Hmmm, that seems impossible. A model for theory T+S is also a model for theory T or theory S.

BTW, can you explain the difference between a set and a type? I asked Hewitt about this previously and didn't get a good answer.

The crude reason that there is no model for CDL because the definition contains deliberate gaps. Someone could ask why you modeled the type "Proof" that way and you will find no textual support for any answer you could give.

Many of the parts of the paper that relate CDL to history provide rationales for those definitional gaps and the resulting blocks on inference. A curious side effect is you get things like the self-consistency proof and the inferential-incompleteness proof -- both signs that the deliberate gaps are well chosen.

BTW, can you explain the difference between a set and a type?

I think so but not very well yet. I'll work on it.

The crude reason that there is no model for CDL because the definition contains deliberate gaps. Someone could ask why you modeled the type "Proof" that way and you will find no textual support for any answer you could give.

Oh I get it. You mean the situation we find ourselves in -- where we propose a model for DirectLogic but then Hewitt drops by to supply a new axiom -- isn't just an annoyance, but is rather the essence of DirectLogic. DirectLogic isn't a single logic, but a family of logics branching through the multiverse.

I think you're being bamboozled.

Edit: Since sarcasm can easily come across as mean, which isn't my intention at all, let me add that I really just mean to express skepticism in the above. There's an air of mysticism about the way that you describe DirectLogic that seems very undesirable to me.

DirectLogic isn't a single logic, but a family of logics branching through the multiverse.

Not quite, no. There's only one universe here.

DL is simultaneously three things:

1. DL is the metatheory of DL.

2. DL is a set of axioms any(?) useful theory can safely include.

3. DL is a meta-theory for all theories that include it.

Since DL is a meta-theory for all theories that include it, all of the theorems of all of those theories are meta-theorems of DL.

In some sub-theories, proofs may be enumerable.

In other sub-theories, not necessarily.

DL, as a meta-theory-for-all, does not assume (or allow you to prove) that proofs are enumerable.

BTW:

I think you're being bamboozled.

If you mean by Hewitt, I don't think so. If you mean by certain commentators making with inane questions or absurd provocations, well, who do you think they are fooling?

The core of CDL is deliberately ambigous in an unusual way. It is not simply that there are multiple possible models of CDL. The ambiguity is deeper than that. There is no model for CDL -- only for CDL plus additional axioms (which we could call the "sub-theories" of CDL).

Hmmm, that seems impossible. A model for theory T+S is also a model for theory T or theory S.

Yeah. I generously read this as saying "minus" instead of "plus." :) It seems to me that if CDL is consistent, any given closed subtheory of CDL has lots of models corresponding to possible extension paths CDL could take -- one of which might be your model that conflates provability with truth-in-the-model.

I think when Hewitt's trying to claim categoricity of the models of integers, sets, etc., there's a sense in which every type in CDL has its own "mini-model" that coexists with the mini-models for all the other types. Once one of these mini-models is categorical in itself, it will remain categorical in every potential model of CDL. (Is there a more standard word than "mini-model"?)

Well, I'm speaking on behalf of a system that isn't rigorous to me and that isn't designed by me, so I can hardly evaluate the truth of what I'm saying.

AFAIK:

Some subtheories have no models because of definitional incompleteness.

Some subtheories have multiple models.

Some subtheories have a unique model up to isomorphism.

(Which kind of describes the territory of mathematical discourse. :-) )

Thanks Thomas!

Sets◅ℕ▻ is a type (unique up to isomorphism), but Sets◅ℕ▻ is not a set in Mathematics thereby providing all of the intuitive sets over ℕ (which is sometimes called "ordinary mathematics").

Separate theories can be provided for more speculative extensions.

I am in two minds about this. On the one hand a finite system makes sense, and is certainly going to be more efficient. On the other hand it is useful to have unbound representations.

I still think I want to separate the ideas of DL from actors, and maybe even the parametric types.

- How would you model integer rings in DL?
- Does the compiler convert sentences into propositions?
- what messages does a type accept?

This probably has minor bugs and more seriously I have no reason to believe it's stylistically any good but;

Group◁σ▷ is the type of all groups using sets of type σ

Every group is defined by a set, along "dot" and "inverse" functions that obey certain axioms.

∀g:Group◁σ▷ ⟶ ∃S: Set◁σ▷, ∙:σ[σ,σ], inv:σσ ⟶
   GroupSpecification[S,∙,inv]
     where
      GroupSpecification[S,∙,inv]
        ⇔   (∀a,b∈S ⟶ a∙b ∈ S) 
          ∧ (∀a,b,c∈S ⟶ ((a∙b)∙c) = (a∙(b∙c)))
          ∧ (∃e∈S ⟶∀a∈S ⟶ (a∙e = a = e∙a) ∧ (a∙inv[a] = e = inv[a]∙a))

By the way, if you are interested in doing abstract algebra, I think(?) you can construct a closed group theory this way:

⊢GroupTheory Φ ⇔ ∃σ:Type, g:Group◁σ▷ ⊢ Φ

Also, after defining ℤ, you could prove:

Theorem: GroupSpecification[Integers, +, 0]

  where ∀i:ℤ, ⟶ 
   i ∈ Integers ⇔ inCountableUniverse[countIntegers[i]]
      where countIntegers[i:ℤ]:ℕ → (i >= 0) ? i * 2 : (abs(i)*2 - 1),
            inCountableUniverse[x:ℕ] → True

I thought DL did not have a universal quantifier?

(Thanks for this question.)

I thought DL did not have a universal quantifier?

The uses of quantifiers here are just a short-hand.

Propositions can be formed according to this rule: 

  If σ1,σ2:Type, x1:σ1 and x2:σ2, then
    x1:x2:Proposition
 
The univeral quantiifer is a short-hand:

  ∀x:σ ⟶ Φ  ≡  x:s ⇒ Φ

The existential quantifier is short-hand for introducting a constant with no specific construction:

  ∃x:σ ⟶ Φ  ≡  x0:Constant◁σ▷ ∧ Φ

In the context of set theory:

  ∀x∈S◁σ▷ ⟶ Φ  ≡  ∀x:σ ⟶ (x ∈ S) ⇒ Φ
                ≡  x:σ ⇒ ((x ∈ S) ⇒ Φ)

  ∃x∈S◁σ▷ ⟶ Φ  ≡  ∃x:σ ⟶ (x ∈ S) ∧ Φ
                ≡  x0:Constant◁σ▷ ∧ (x0 ∈ S) ∧ Φ


For example, the group theory axioms begin:

  ∀g:Group◁σ▷ ⟶ ∃S: Set◁σ▷, ∙:σ[σ,σ], inv:σσ ⟶
     GroupSpecification[S,∙,inv]
      where [...definition of GroupSpecification...]

which could be (less expressively but equivalently) written:

  g:Group◁σ▷ ⇒
      Sg:Constant◁Set◁σ▷▷
    ∧ ∙g:Constant◁σ[σ,σ]▷
    ∧ invg:Constant◁σσ▷  
    ∧ GroupSpecification[Sg,∙g,invg]
      where [...definition of GroupSpecification...]

So this would allow a model of say 64bit integers? I am slightly concerned about the size of the model, as in its not what would would call a concise description.

Back to my dilema. Starting with machine integers, and zero terminated strings, we can model unbounded integers starting from machine words (bounded by the addressable memory of the machine implemented on).

Which is the better approach? At the moment I still prefer starting with the machine word and building up, as it mirrors the real world.

In fact the two may be complementary, DL being top down, and implementations being bottom up.

I think I missed one axiom here:

∀g:Group◁σ▷ ⟶ ∃S: Set◁σ▷, ∙:σ[σ,σ], inv:σσ ⟶
   GroupSpecification[S,∙,inv]
     where
      GroupSpecification[S,∙,inv]
        ⇔   (∀a,b∈S ⟶ a∙b ∈ S) 
          ∧ (∀a,b,c∈S ⟶ ((a∙b)∙c) = (a∙(b∙c)))
          ∧ (∃e∈S ⟶∀a∈S ⟶ (a∙e = a = e∙a) ∧ (a∙inv[a] = e = inv[a]∙a))


By the way, if you are interested in doing abstract algebra, I think(?) you can construct a closed group theory this way:

⊢GroupTheory Φ ⇔ ∃σ:Type, g:Group◁σ▷ ⊢ Φ

An additional axiom is needed to express that if a set, dot operator, and inverse operator exist that satisfy the axioms, then a corresponding group exists.

∀σg:Type, Sg:Set◁σ▷, ∙g:σ[σ,σ], invg:σσ ⟶ 
  GroupSpecification[Sg,∙g,invg] ⇔ g:Group◁σ▷

Finally, closure. Groups are uniquely identified by their components:

∀σ:Type, g,h:Group◁σ▷ ⟶

  g = h ⇔   (Sg = Sh)
          ∧ (∙g = ∙h)
          ∧ (invg = invh)