Lambda the Ultimate

Addresses of Actors can be sent in messages.

Of course, a procedure is an Actor, which can be invoked by sending it arguments in a message.

So if I have an actor that passes its own address to the actor address passed to it, you have the Y-combinator, which calculates the fixed point. I thought fixed points were not possible?

Types mean that fixed points do not exist in ActorScript and Direct Logic.

What prevents me declaring the Y-Combinator then? Which specific typing rule?

I have seen in the examples procedures which call themselves (like the factorial example), so if a procedure can pass a message to itself, and can pass its address as a message to another procedure, you can create the Y-Combinator.

The Y combinator cannot be defined using ActorScript:

 
PropToProp ≡ [Proposition]↦Proposition
Helper.[f:PropToProp]:PropToProp ≡ [x:([⍰]↦PropToProp)]→ f[x.[x]] 
Fix.[f:([PropToProp]↦PropToProp)]:PropToProp ≡ (Helper.[f]).[Helper.[f]]

The missing strict type ⍰ does not exist.

Factorial∎[n ←9, accumulation ←1] ≜
 n � 1 ⦂ accumulation⦶
 (> 1) ⦂ Factorial∎[n–1, n accumulation] ⍰▮

I can only easily type ASCII, so hopefully you can understand the following without the specific unicode characters:

Y.[f] = f.[Y.[f]].

How do I indicate 'f' is the address of an Actor? How does the type system deal with addresses of Actors?

With types made explicit:

Factorial.[n:Integer]:Integer ≡
 n=1 � True ⦂ 1
        False ⦂ n*Factorial.[n–1]

However, Y.[Factorial] is an infinite loop with the following (mistaken) definition of the Y combinator:

Y.[f:([Integer]↦Integer)]:Integer ≡ f.[Y.[f]]

I can give typed Y combinators in Haskell and ML; with some verbosity in C++ even. It isn't hard, I needed to think about the ML version for half an hour and naturally defined an eager version for it.

Why would I use Actorscript if I can naturally define a Y combinator in most other typed languages?

The Y combinator is not practically useful for anything.

Since my small declarative language doesn't have local recursive function definitions I use it all over the place?

But, granted, in a better language you don't really need it. But it's a nice to have if it can be expressed.

It just shows other languages have more expressive type systems than Actorscript. So, I won't use Actorscript.

The Y combinator is an obscure, convoluted hack to do recursion :-(

Works fine in my language.

    def fix: ((a -> b) -> a -> b) -> a -> b =
        [ f -> f [x -> (fix f) x] ]

    def long_to_text: long -> text = 
        zero = int_to_long 0;
        ten  = int_to_long 10;
        c = [ 0 -> '0' | 1 -> '1' | 2 -> '2' | 3 -> '3' | 4 -> '4'
            | 5 -> '5' | 6 -> '6' | 7 -> '7' | 8 -> '8' | 9 -> '9' ];
        p = fix [ p, nil,       x -> cons x nil
                | p, cons y yy, x -> cons y (p yy x) ];
        s = fix [ s, n ? n < zero    -> cons '-' (s (zero-n))
                | s, n ? n < ten     -> cons (c (long_to_int n)) nil
                | s, n            ->
                    n0 = n / ten; n1 = n - (n0 * ten);
                    p (s n0) (c (long_to_int n1)) ];
        [ n -> _txt (s n) ]

The Y-Combinator is a natural consequence of having recursion and first class functions. It looks like you allow general recursion, which must mean you do not have first-class functions. You claim you can pass the address of one actor to another (which would seem to be similar to first-class functions) so I am trying to understand the details of the difference (because the exact details are important).

Types mean that the Y combinator can't be implemented in ActorScript

Which is a great reason not to use ActorScript.

"Since my small declarative language doesn't have local recursive function definitions I use it all over the place?"

I realize that code generation is a bit more complicated with recursion, but let me guess that you don't have looping constructs either - so if you want efficient looping you need to handle recursion specially anyway.

I like minimalism. I don't handle recursion in any special manner, it's just that only top level definitions may refer to themselves - each top level definition becomes a (trampolined) C routine.

I left it as a 'nice to have' for some later version.

So what is the restriction that prevents that definition of the Y combinator? [Interger]->Integer and Integer both seem reasonable types?

The Y fixed point procedure on integers is not valid because types must be constructively defined:

IntegerToInteger ≡ [Integer]↦Integer
IntegerFunctional ≡ [IntegerToInteger]↦IntegerToInteger 
Nonexistent ≡ [Nonexistent]↦IntegerFunctional    // not allowed

Helper.[f:IntegerFunctional]:Nonexistent ≡ 
  Let g.[x:Nonexistent]:IntegerFunctional ≡  f[x.[x]]｡ 
    g 

Y.[f:IntegerFunctional]:IntegerFunctional ≡ (Helper.[f]).[Helper.[f]]

Edit: For example, the following is a valid definition of an Integer functional:

FactorialFunctional.[f:IntegerToInteger]:IntegerToInteger ≡
   Let g.[n:Integer]:Integer ≡ 
          n=0 �
            True ⦂ 1
            False ⦂ n*f.[n-1]｡
     g

Consequently, FactorialFunctional[Factorial] is equivalent to Factorial.

I'm obviously still not getting it. I don't even see why you need "Nonexistent". Surely the type you want for an integer fixed point is:

Y : [[Integer] -> Integer] -> [Integer] -> Integer

So you could pass a function like:

f x = x + f (x / 2)
Y f 1

Should return the result 2. The first argument to Y is clearly a function from integer to integer, the second argument is simply an integer, and it returns an integer. There are no complicated or unrealisable types. Of course the definition of Y at the value level might be tricky, but it is certainly well typed.

It is important for types that Y definition (above) is not valid.

Invalid types like Nonexistent (above) are not constructively defined.

Aside from why you might not want to allow them, I don't really see what you are disallowing. So do you not allow higher order functions (actors), where the argument of one function is another like:

[[Integer] -> Integer] -> ...

Or do you not allow functions that return functions like:

... -> [Integer] -> Integer

Edit: I might have a vague clue that you don't allow construction of a function like 'Y', but I am not sure how. I don't see why you need "nonexistant"? Surely you just need IntergerToInteger and IntegerFunctional. The type of the function you want to calculate the fixed point of is "IntegerToInteger" and the type of the Y combinator is "IntegerFunctional". It seems you can define the Y combinator without "nonexistant", so why is it even there?

The Y fixed point procedure has a definite definition that has no valid types.

That's an odd way of putting it. Don't you mean the procedure fails to type check?

The question is why it fails to type check? Let's start with valid types;

fix<a> = [[a] -> a] -> [a] -> a

Ignoring what procedure has this type, and how the type is generated, is the above a valid type for a procedure?

The parameterized Y◅aType▻ fixed point procedure is not valid because types must be constructively defined:

SingleArugment◅aType▻ ≡ [aType]↦aType
Functional◅aType▻ ≡ [SingleArugment◅aType▻]↦SingleArugment◅aType▻
Nonexistent◅aType▻ ≡ [Nonexistent◅aType▻]↦Functional◅aType▻   // not allowed

Helper◅aType▻.[f:Functional◅aType▻]:Nonexistent◅aType▻ ≡ 
  Let g.[x:Nonexistent◅aType▻]:Functional◅aType▻≡  f[x.[x]]｡ 
    g 

Y◅aType▻.[f:Functional◅aType▻]:Functional◅aType▻ ≡ (Helper◅aType▻.[f]).[Helper◅aType▻.[f]]

Let's suppose:

  factorial == Y[fixes-as-factorial]
            == fixes-as-factorial[Y[fixes-as-factorial]]


  shorthand:

  faf == fixes-as-factorial
  n2n == [Natural] |-> Natural

  i.e.

  factorial : n2n

  factorial == Y[faf] == faf[Y[faf]]

  faf's type?  One could say:

  faf : [typeof(faf)] |-> n2n 

  but...

A few DL types are primitive.

Additional DL types may be introduced by deriving a new type that is distinct from all earlier defined types.

No other types exist.

Notice that the purported type of faf is:

  faf : [typeof(faf)] |-> n2n 

To construct the type of faf one must have already constructed the type n2n and also the typeof(faf) itself.

Since the type of faf must be constructed before it can be constructed, it must not exist.

But I can have a simple function with the same type as the fixed point. For example:

g f = \x . f (f x)
has the type 
g<a> : [[a] |-> a] |-> [a] |-> a

And I can pass it a function like increment by one, and 'g' will return a function that will increment by 2.

This has the same type as the fixed point, but performs another calculation.

So as far as I see, there is nothing wrong with the _type_ of the fixed point function.

Now consider "Mathematica", we could pass a symbolic representation of the function 'f' to a fix function that performs algebraic manipulation of the symbolic representation and returns the fixed-point (for example calculates the fixed point of infinite arithmetic or geometric progressions).

In that sense 'Y' can be defined as a meta-function that operates on functions without any self-referential definitions.

edit: I think I see, the type equation solver is not able to solve a type like :

X = X |-> X

So effectively you don't allow some generalisations of type variables? Because traditionally:

X = forall a . a -> a
X = forall a . (a -> a) -> (a -> a)
X = forall a . ((a -> a) -> (a -> a)) - ((a -> a) -> (a -> a))

The top (a -> a) is the most general type and it includes all those below. Now we know the AcrorScript types we are discussing don't have universal quantiication, but we can represent the above parametrically:

X<a> = [a] |-> a

Now we can provide "[a] |-> a" or "[[a] |-> a] |-> [a] |-> a" as the parameter to the above type X.

So the type of "faf" can be derived to be:

faf<a> = [a] |-> a

Which I guess would become an infinite expansion:

faf<a> = [a] |-> a, 
[[a] |-> a] |-> [a] |-> a
etc...

So it appears the important bit is the difference between parametric and universally quantified types, although we could recover the Y combinator with parametric types by permitting recursive types, which using "mu" notation would give something like the type:

f<a> : [a] -> a
Y : mu b . f<b>

The Y fixed-point procedure itself has a typed signature; but its implementation is not typed.

So effectively you don't allow some generalisations of type variables?

I guess you could say that.

Types are defined by a constructive induction. Therefore they are partially ordered by a kind of ranking.

The lowest ranked types are: Boolean, ℕ, Sentence, Proposition, Proof, Theory.

New types may be constructed from earlier constructed types. For example if σ₁, σ₂:Type then there is a function type: [σ₁] ↦ σ₂.

A function type is of higher rank than it's domain and codomain.

Consequently, a function type is always distinct from its domain and codomain.

Hewitt's earlier described helper function and my "faf" (fixes as factorial) both have the same, non-existent type.

   We know:

   factorial : [ℕ] ↦ ℕ

   Assume to derive a contradiction that:

   factorial ≡ Y.[faf]

   where

   Y : [typeof(faf)] ↦ [ℕ] ↦ ℕ

   and where Y, defined in the customary way, gives us:

   Y.[f : typeof(faf)]:[ℕ] ↦ ℕ ≡ Helper.[f].[Helper.[f]]

   since we know that Y.[faf] is factorial we can, read off
   the domain and codomain of Helper:

   Dom(Helper) ≡ typeof(faf)

   Cod(Helper) ≡ [ℕ] ↦ ℕ

   that is to say:

   Helper : [typeof(faf)] ↦ [ℕ] ↦ ℕ

   the whole concept of faf, which when fixed yields factorial,
   is that faf applied to itself is factorial.  From this it follows
   that we can read off the type of faf:

   faf : [typeof(faf)] ↦ [ℕ] ↦ ℕ

   By inspection we can see that the types of faf and Helper
   are the same and therefore:

   Helper : [typeof[Helper]] ↦ [ℕ] ↦ℕ

   these constructions don't work, in DL because they have it that:

   Dom(faf) ≡ typeof(faf)

   and

   Dom(Helper) ≡ typeof(Helper)

   yet in DL, a function type can only be defined in terms of a
   lower ranking domain and a lower ranking codomain.

So, no, types don't "generalize".

Interestingly, a syntactically recursive definition of factorial is perfectly fine.

   factorial.[x:ℕ]:ℕ ≡ if (x = 0) 1 else x * factorial.[x-1]

and as Hewitt has mentioned we can define a (particularly uninteresting) functional:

  FactorialFunctional.[f:IntegerToInteger]:IntegerToInteger ≡
     Let g.[n:Integer]:Integer ≡ 
            n=0 �
              True ⦂ 1
              False ⦂ n*f.[n-1]｡
       g

and thus FactorialFunctional.[Factorial] is equivalent to Factorial.

Still, FactorialFunctional is not a function that when self-applied yields Factorial.

Okay, I think I now understand what is going on with the type system. It seems it has big-lambda and no universal or existential quantification, so in more common type system notation we would write:

Y<a> = [[a] -> a] -> [a] -> a

as

Y : \a . (a -> a) -> a -> a

I think that captures all the same properties, except the message arity, which I am not concerned with for the moment.

Edit: I am again a bit confused, what happens with something like the identity function:

id : forall a . a -> a
id x = x

If this were written with a type parameter you would get something like;

id : \a . a -> a 

However there is only a single function here, so if we try and use it:

id "hello"
id 27

We cannot bind it to two different types. It is the universal quantification of the type variable that allows it to be both a string and an integer at the same time (as there is only single function).

How can we define a re-usable polymorphic function without universal quantification?

How can we define a re-usable polymorphic function without universal quantification?

Every function has a definite domain and co-domain. There is no "any" type.

In ActorScript, a "parameterized type" can be defined. The class of typed identity functions could be defined (modulo my ActorsScript errors):

  SingleArgument◁aType▷ ≡ [aType] ↦ aType

  Id◁aType▷ ≡ 
    Actor implements SingleArgument◁aType▷ using
      [x] → x ▮

Actorscript supports "polymorphism" in roughly the manner of "generics". Different actors can implement the same type as one another using different implementations.

A longer example begins on page 33 of the ActorScript paper.

p.s.: Hewitt - the appendix 4 hex value for "end" (▮) is wrong.

Thanks for noticing the typos!
They will soon be corrected on HAL.

It also possible to define Id as follows:

Id◁aType▷.[x:aType}:aType ≡ x ▮

Is there an already existing Emacs abbrev file somewhere to translate IDE ascii into the assorted unicode used by DL and ActorScript?

There is something odd here. There is only one 'id' function, so once you have grounded its type parameter to say Integer, it is only integer and cannot be anything else at the same time.

A polymorphic function like Id can be applied to arguments of any type that has the property that the definition of Id type-checks if "aType" is replaced by the type in question.

It so happens that the definition of Id is such that it will type check no matter what type you replace aType with.

Other polymorphic functions are not necessarily that general.

In other type systems, there is only one id function. It can only have one type. The universal quantifier says this single id function accepts any type, but there is still only one id function. You can think of this in the code output by the compiler itself, there is a single function that accepts any type.

So a type with a parameter like: \a . a -> a once bound to an Integer can only accept integers, and hence the same function cannot be used on strings as well.

In ActorScript types this is different because there is some kind of assumed operation on the functions (probably elaboration like Ada generics), where every time we use a function like id on a type we have to make a copy of it, and elaborate it on that type to generate a specialised id function. We then have to keep track of every type id is already elaborated on, so that we don't proliferate unnecessary copies of the function.

At the moment I cannot think how to represent such a constraint in a formal type system, I suspect it requires introducing the notion of a set of types, something like:

{\a . a in T => a -> a}

IE we have a set of functions each of which accepts a type parameter which must be in the set of types T which is all the types the function is applied to in the whole program.

You can think of this in the code output by the compiler itself, there is a single function that accepts any type.

Would that not depend on the language and the compiler? In the examples that I've seen the function would be specialised to a type signature, so that in the generated code there would be a function id_integer_integer and another id_string_string. They would both have originated from a common description but at the point that they were instantiated over a concrete type they became separate functions. This depends on what style of polymorphism is in use. C++ uses this approach and then mangles the types into the names. I think (very fuzzy memory) that Haskell does the same, or it throws an error at the point that the function cannot be instantiated with the types (i.e. the constraints cannot be met)?

The claim that there is only one id function is after all just a claim that is relative to what is syntactically valid. If one is working in a system without polymorphism at all then it is clear there is no universal id function. If one is working in a system where polymorphism defines a template that can be instantiated into functions, then the universal id is not actually a function.

I think the type system, as related to a logic, or an algebra has these intrinsic properties. I don't think C++, Java etc, have a proper algebraic type system.

Haskell types are implicitly universally quantified, and you can read them as:

id :: forall a . a -> a
id x = x

With exactly the semantics I describe above.

The claim about only one id function is based the logic underlying the type system, nothing to do with the language or its semantics.

Soundness is defined by a type system that admits only well formed programs, IE the logic of the type system matches the semantics of the language. Therefore it must be possible to have unsound type systems (where the logic does not match the semantics) and even type systems with no language.

Simply saying:

a -> a

Without introducing 'a' is not a complete statement, a is free in the expression, and it must be introduced in order for this to be a meaningful statement in logic, for example:

\a . a -> a
forall a . a -> a
exists a . a -> a

'->' is just an infix functor (logic terminology, not category theory). You could alternatively write:

\A . arrow(A, A)

Using upper case for logic variables and lower for atoms. The problem is, for none of these options above does the logic match the semantics of ActorScript types.

What is it about the DL types that you find odd? Isn't this scheme just restricting to no higher rank polymorphism? He seems to be calling quantified types "roughly generics" and distinguishing them from types. This corresponds to requiring all quantifiers be at top level in types. Also, look at the System F encoding of Haskell types. A value of quantified type is encoded as a function using big lambda.

So in system F, "id" is:

|- /\a . \x^a . x : forall a . a -> a

So the type is still universally quantified. ActorScript types we are told have no universal quantification.

You cannot assume free variables are universally quantified, see:

http://math.andrej.com/2012/12/25/free-variables-are-not-implicitly-universally-quantified/

In System F, you'd have id = \a:*. \x:a. x. I understand him to be saying that id isn't a proper value, but is a family of values. In other words, he considers (id Int) and (id Char) to be values, but id isn't a proper value. Quantified types in System F would correspond to "types" of these families, but he doesn't call them "types", a term he reserves for ordinary types of values. So (\a:*. \x:a. x) has a "family type" of roughly (forall a:*. a -> a). But he doesn't allow function families to be passed first class - no higher rank polymorphism.

I'm filling in some blanks, but this setup doesn't seem particularly unusual to me.

So what extensions to a simply typed lambda calculus would be needed to support this kind of typing?

I am not saying its unusual (Ada generics work this way) but they are largely ad-hoc. How would this relate to a formal type-system, or to logic?

Edit: I think I am thinking of the type level lambda the wrong way. Perhaps the actor type for "id" could be written:

/\a . a -> a

I think you just need to split the grammar for System F so that family values (big lambda) and family types (forall) don't produce ordinary values and types, but rather produce value families and type families:

V = x | \x:T. V | V V | primitive
VF = V | \a:*. VF
T = a | T -> T | primitive
TF = T | forall a:*. TF

Edit: And to answer your second question... I'm not arguing that it's a great type system. Just that it doesn't seem particularly odd to me.

So with a universally quantified type we can translate to logic quite easily, using Prolog syntax:

forall a . a -> a   <=>   arrow(A, A).

What would an actor type look like with the implicit universal quantification of the Prolog clause. Clauses have implicit universal quantification. If we take that away, once a clause is bound to a value, it retains that value for the rest of the program (generalisation does not happen).

We could imagine abstracting the values from the Prolog clause using a lambda as in:

\A . arrow(A, A).

Now I guess we have to know the argument 'A' before we can match and unify the clause. It seems kind of useless as a logic because we can no longer return a value, or propagate an unknown type.

Family polymorphism would only exist at top level. If you want to pass a value first class you have to choose a (non-family) type for it. I agree that this makes for a weak logic.

Presumably you have to choose first, which means you cannot operate on unknown variables, which would seem to make inference harder.

How would you adapt system-F to support both the normal universal quantification, and types like Actor Script types?

How ActorScript types work in the first place is already a good question, but at the moment I suspect it's very close to System F and the kind of polymorphism you expect. Here's something Hewitt said elsewhere in the thread:

PS. Also, it is possible to define Fix◅aType▻ although that doesn't create an untyped fixed point to create "self-referential" sentences.

I fixed the misleading statement in my previous post.

There is a signature but no valid implementation of Y◅Sentence▻. There are no "self-referential" sentences in Mathematics.

I don't see how a fixed point combinator would lead to "self-referential" sentences anyway. To me, they're independent topics at the moment. (Maybe there's something I'm missing.)

Per Martin-Löf wrote (in "Constructive mathematics and programming", in "Proceedings of the sixth international congress for logic, methodology and philosophy of science," 1982):

I do not need to enter the philosophical debate as to whether the classical interpretation of the primitive logical and mathematical notions (proposition, truth, set, element, function, etc.) is sufficiently clear, because this much is at least clear, that if a function is defined as a binary relation satisfying the usual existence and unicity conditions, whereby classical reasoning is allowed in the existence proof, or a set of ordered pairs satisfying the corresponding conditions, then a function cannot be the same type of thing as a computer program. Similarly, if a set is understood in the sense of Zermelo, as a member of the cumulative hierarchy, then a set cannot be the same kind of thing as a data type.

It is a classical notion, of the sort from which Martin-Löf removes himself, that one can say:

In other type systems, there is only one id function. It can only have one type.

That is problematic in a constructive type theory since it entails the existence of a "type of all types".

The type-parametric definition of Id◅aType▻, illustrated in earlier comments, is not a constructively well-defined function because it has no definite type: no domain and codomain. It is "something else", not a "function".

The type-parameteric Id◅aType▻ can be regarded as a kind of idiosyncratic mathematical object. The parameterized type signature is one kind of abstract grammar tree that describes a class of function types. The full generic definition of Id is a grammar tree that describes a class of Actor implementations. (It is really an internal detail of implementation whether or not the class of Actor implementations can all be compiled to a single machine code or whether different members of the class must be compiled separately).

In addition to being a programming language, Actorscript is a suitable language for expressing DL terms, such as the definitions of mathematical functions.

If you are coming from a classical-logic-and-set-theory point of view that might seem odd because, well, it is different from that tradition.

I am not really in a position to defend these people because my own opinion is that there are too many mathematicians and logicians in CS, subsequently SE is both misunderstood and taught badly, but the title is more or less the argument.

We want correct software. One manner of achieving that is through formal means, proving software correct. The problem with proving software correct is that maybe Godel blew up that idea a priori. Therefor there is a need to establish maximally strong logical frameworks to prove software correct. Hewitt thinks he did that with a certain logic I don't understand.

That's about it.

Inconsistency Robustness is the best we can do for large software systems, which are pervasively inconsistent.

My software works.

Why do Windows, IoS, Linux, etc. always have huge numbers of bugs?

Whatever gave you that impression? My software just runs? Actorscript cannot prevent the occasional 'logical' (algorithmic design) bug from appearing either; how does it prevent division by zero errors?

In practice, my software works and I have uptimes of years.

"too many mathematicians and logicians in CS"

Especially in the field of programming languages there's a difference between an engineer and a mathematician.

Mathematicians usually start with severely limited domains because in any new area, you can usually only write proofs about things that are very simple and limited... even as an area evolves, the mathematical notations for it remain as minimal as possible because being able to write proof is enough.

An engineer wants tools that are expressive and that's the opposite of limited. Also an engineer just wants to be able to write something that he can reason about - he doesn't need a proof let alone a automated proof. A system that's designed to prove various (often trivial) properties about his programs may just get in the way of getting the work done. It may make the work impossible, even.

Yeah well. There's that and there's that (despite that there are scientists which are great engineers), often, they'll simply get everything wrong.

It's a real hassle. In the small country I live in, students who want to go to a university after college are advised to not go to CS departments with a high theoretical focus because they'll a) will not learn an additional skillset, and b) will need to unlearn lots of stuff when entering industry from that department.

Unless you want a career as a scientist, there's simply not much there in most theoretical CS departments. And even what is there is often somewhat dubious.

(Don't blame me, I didn't know either until I became a college lecturer.)

I'm not even convinced that types are good for programming.

For one thing I've noticed that everything you can do with types that actually effects the result of a computation (rather than limit what can compile) could also be written in something like in prolog, and the prolog would be much more expressive and less limited.

As for types that are there to prove that your program does the right thing... well not everyone needs that, not all the time. And most of the time, the style of programming it forces is a lot slower than the alternative.

People writing in overly typed languages have to solve TWO problems, one is the algorithm - the other is fitting it into the type system. If you delete the second problem, a lot of problems become trivial.

Types ARE a language, but they're one of those severely limited domain languages that mathematicians love because they can make proofs about them.

But no one here even seems to notice expressiveness. Lack of limitations may make programs hard to make proofs about, but they make them easier to write.

And for god's sake they're arguing about the y-combinator, something that is useless in any real language where a function can refer to itself. Why would they assume a function can't - oh they had some calculus where they thought they couldn't make a proof if functions could refer to themselves. Useful in the real world? Absolutely not.

Yeah well. Parsing is 2% of the effort of implementing a compiler and typing is maybe another 10%.

Typing for a programming language, well, someone should write a good book about it once because I gather it's a mostly finished subject.

It's just one of those things you can produce nice greeklish about which will get published because it looks sciency. It's also surprisingly hard to get right, so that doesn't bother me too much, but anyone who thinks a compiler is about parsing and typing is a fool; and it looks CS delivered another generation of those.

The type-theory academics have this deep belief, I think, that if they can just keep at their approach until they get it right enough it'll be so wonderful that it'll win everyone over. Which may be true... it's good that academia can explore things like that with very long lead times... but in this case I think they're barking up the wrong tree. Your point about two problems, one algorithm and one typing, seems closely related to the argument I've been making lately against types. It's a little scary to me that I've gotten some objections when I suggest that the first duty of program syntax is to be readable. By which I mean, clearly express the algorithm. Types, I've concluded, are essentially a tying of program syntax to reasoning about programs (through the imho over-hyped Curry-Howard correspondence), but once you tie program syntax to both things, the demands of making these two things clear pull the syntax in different directions. If correctness proofs are to be practical, you need proof and algorithm both to be clear, which you can't get if you tie both to a single syntax.

one end point of programming is where you specify a problem and the software is the programmer.

We may even get there eventually.

I know none of what they're arguing about is declarative programming but I'm still tempted to make the joke that mathematicians imagine that what they need to get right is the ability to specify problems and the magical programmer in a box is a trivial problem left up to the reader.

But I do notice that nothing on this blog is about algorithms, at best it's about trivial classifications of algorithms, such as whether they can be proved to terminate.

Donald Knuth seems a likely counterexample.

I've felt strongly for decades that the mental talent needed to write a good program is the same as needed to write a good proof, making it fascinating that there's this huge gulf between the two disciplines. Revisiting that insight now, I'd add that it's crazy to try to constrain the syntax such that the same syntax is ''both'' a good program ''and'' a good proof at the same time. A bit like trying to come up with two grammatically correct sentences in two different languages such that the two sentences sound the same.

It would be interesting to me if you could come up with a proof syntax and a program syntax - keep them separate and show a program and a second meta-program that declares things about it or proves things about it.

Assume that I can't already read the notations they use around here and describe whatever one you come up with.

I already realize that there are some programming constructs that will throw monkey wrenches into proofs... I think we both agree that you have to allow those and that you should also be able to tell your prover to assume things that it can't prove. Such as my trivial example that a REPL will eventually end its loop (because the user won't want it to run forever).

As an aside I don't think that proof of termination is usually useful.

I have something like this, the proof language is like Prolog and the programming language is effectively a lambda calculus.

Types are inferred from the lamdba calculus, and these becomes the terms in the meta-language.

that I've failed to find reference to. It was a microsoft thing with a research version of a their SAT solver that they never released. It was making proofs about routines in a subset of C#

But I don't remember it showing any code, just talking about it.

They apparently used it to prove some properties about a security protocol routine. That was the selling point, that you could use proof to improve security. SAT solvers are supposedly pretty good at proving that there is no input that will break something, or finding an input that will.

It's a bit mind boggling though, the gap between proving something about some code using types and sicing an advanced SAT solver on the code to try to break it.

My SAT solving enthusiasm has tempered considerably since I started experimenting with it. The initial selling point was that it could solve problems with thousands, or orders more, of variables.

Turned out that all these variables are the result of translating a digital circuit into CNF. I.e., a NAND term 'x|y' becomes 'z <=> x|y' becomes '(-x \/ -y \/ -z) /\ (z \/ x) /\ (z \/ y)' according to the following table.

x y z
0 0 1
0 1 1
1 0 1
1 1 0

A digital circuit is trivially translated to CNF by assigning each out gate a variable and using the above encoding.

All those 'thousands' of variables just imply a SAT solver is a very efficient manner of finding truth assignments over a digital circuit. But, unfortunately, it looks like all NP results hold, and maybe one can check little more difficult circuits than through old means of finding assignments over circuits. SAT solvers are simply efficient because the CNF representation is aimenable for a solver written in C; i.e., the CNF representation fits neatly into arrays and arrays can efficiently be locally accessed.

Looks like Knuth dove down the same rabbit hole, so I guess I am in good company, but fundamentally nothing much changed. It's just efficient local search.

(Satisfiability modulo theories) not that I really understand SMT. SMT solvers can solve constraints over specific theories or combinations of them. So the programming one probably knows something about arrays and numbers not just booleans.

I rented a text book on it, and was very sad to note that I tried to convert the rental into a purchase a few days too late to get rental as credit toward the purchase. $40 down the drain. >.>

That said I didn't read enough to understand the magic... And there are new algorithms that weren't in the book, more efficient ways to combine theories.

I have some thesis bookmarked though.

Microsoft claims to have an unreleased SMT solver for symbolic solutions to nonlinear equations that they claim is almost as powerful (and as fast) as Mathematica on them. I've forgotten what that kind of solver is called. Eliptical something :/

I remember some papers on solvers. Someone first siced a boolean SAT solver on a bunch of constraint problems, treating each bit of the numbers involved as a separate variable. It beat every mini-zinc solver around.

Then he did another paper where he tried an SMT solver that had theories about numbers and maybe a few other things. It beat the simple SAT solver and also all of the traditional constraint solvers.

Note that the constraint solvers could use search space hints and the SAT and SMT solvers couldn't - but SAT and SMT still beat them.

It'll likely depend on the problem. SAT solvers will likely 'discover' good manners of searching the search space if they are there; even strange strategies you wouldn't think of yourself so the hints one can provide are probably superfluous.

But if you start doing SMT which is roughly combining many techniques the problem matters the most. If you're simply not doing a lot of propositional reasoning a SAT solver becomes overhead over pure symbolic reasoning; it's likely that trivial. So I somewhat expect pure 'chaos' as the outcome of comparing SMT solvers.

SAT solvers are commonly used in industry because, even though they take exponential time in the worst case, they're efficient for large classes of problems. In some domains, the "exponential time" worst-case is nowadays a mostly theoretical concern. One example I'm somewhat familiar with is discussed in http://arxiv.org/abs/1506.05198 (though I didn't read that particular paper yet).

Of course, if you have a genuinely NP-complete problem, translating to SAT probably won't help; but often it's easier to encode your problem for a SAT-solver than to figure out a specific algorithm specializing all the SAT-solving heuristics to your domain.

The models in the paper aren't very large. 64K variables sound large but isn't when you got in the back of your mind that that corresponds to a digital circuit of 64K gates; that's pretty small.

Moreover, the experiment is ran on models which encode implication chains I gather. That's not that difficult for a SAT solver.

Sat solving becomes exponentially harder on trivial problems like multiplication.

So. Nice application domain, though a bit cherry picked.

I never claimed SAT solvers aren't without their use; but given the initial enthusiasm of solving NP problems maybe within reach, I can only conclude they (mostly) didn't made a dent into those problem.

if it was Knuth or Dijkstra who hated lisp, but one of them was made ill by the notion of algorithms that can do things that make proofs impossible, said that the punning between data and code was an abomination.

It just shows that someone whose job is to prove things about algorithms has totally different needs than someone whose job is to write programs.

By the way, what I'm going to be doing for a few hours is to turn a normal language into a homoiconic one by adding an accessable parser and parse tree format and embedding such things in. I guess all these proof obsessed people don't see much use for homoiconic languages. Prolog was homoiconic without being unreadable, but that sort of advance disappeared with it. Haskell isn't homoiconic, notice.

As I recall, McCarthy defined Lisp in Lisp as a demonstration of mathematical superiority of the language.

On the very first page:

The second important part of the LISP language is the source language itself which specifies in what way the S-expressions are to be processed. This consists of recursive functions of S-expressions. Since the notation for the writing of recursive functions of S-expressions is itself outside the S-expression notation, it will be called the meta language. These expressions will therefore be called M-expressions.

Third, LISP can interpret and execute programs written in the form of S-expressions. Thus, like machine language, and unlike most other higher level languages, it can be used to generate programs for further execution.

The language was defined via a recursive function notation called M-expressions. A program in lisp was able to interpret a lisp program expressed as S-expressions, but this put it in a practical category alongside machine language rather than a vague "mathematically superior" category.

LISP had the practical advantage that you could write programs that would generate and then execute code.

SCHEME (after its AI lab days) did its best to turn its back on this practical utility and struggled to hint vaguely at some kind of quasi-mathematical utility. Because hygiene and lexical scope and CPS and Strachey or something.

early standards of scheme didn't specify eval, though most versions had it.

Also I guess taking it out, or pretending it isn't there allows a bunch of optimizations and I think some people in scheme wanted to focus on the optimizations.

"LISP had the practical advantage that you could write programs that would generate and then execute code."

That's not enough. I want languages that have libraries to help you analyze code, transform it, specialize it, optimize it...

Why did the lisp community never get too deeply into metaprogramming?

For that matter, why not have nice parser? At least the guy who invented FORTH had the excuse of not being an expert in CS.

Why did the lisp community never get too deeply into metaprogramming?

Well, here's some interesting deep magic I noticed when researching my dissertation.

My topic, of course, was fexprs, and as I think I've remarked at some point or other on LtU, I've always had at least half in mind that an interpreter for a Lisp with fexprs might be run at "compile" time to generate the compiled image of a program, to interestingly useful effect. Let's put a pin in that and come back to it.

Turns out that Shriram Krishnamurthi in his dissertation — which I couldn't have helped noticing since he was on my dissertation committee — was proposing something he called micros, which are a bit like macros except that where macros do a transformation from source-language to source-language, micros do a transformation from source-language to target-language. When a micro wants to it can recursively invoke the compilation process to transform any source-language expression into the target-language, using a function called dispatch. Which is uncannily similar, in a sort of inside-out way, to what fexprs do. From my dissertation:

Each fexpr specifies a computation directly from the (target-language) operands of the fexpr call to a final result, bypassing automatic operand evaluation and thus giving the programmer complete semantic control over computation from the target language. Each micro specifies a translation directly from the (source-language) operands of the micro call to a target expression, bypassing automatic operand translation and thus giving the programmer complete syntactic control over translation from the source language. Thus, micros are to translation what fexprs are to computation. The parameters of the analogy are that micros bypass processing that would happen after a macro call, and are inherently syntactic; while fexprs bypass processing that would happen before a procedure call, and are inherently semantic. The analogy also extends to internal mechanics of the devices: micros [...] rely heavily on a function dispatch that explicitly performs source translations, compensating for the loss of automatic operand translations — just as fexprs (treated here) rely heavily on a function eval that explicitly performs evaluations, compensating for the loss of automatic operand evaluations.

When you start comparing fexprs at compile-time to micros... I suspect fexprs turn into a more fluent device subsuming the capabilities of micros.

I've actually made a couple of macro systems with the specific idea in mind that I'm making a Kernel-style fexpr phase. It's pretty nice for defining local macros, because it's just a matter of appending a binding to a first-class environment.

I also return dedicated AST objects--much like a target language expression, but potentially with extra methods like listing the free variables or doing some visitor pattern code-walking. Since I haven't put my own languages to much actual use, I'm not quite sure what methods I'm going to want yet.

using a hidden code to code translator and taking advantage of the fact that it's a dynamic language.

Lua might not be to the taste of people here, but it's popular enough, has a tiny, fast tracing jit. And it has a guarantee of tail call elimination.

That ought to be enough to bestow on it all sorts of powers.

It also has the advantage of being really simple and small.

The one thing it's missing is threads. It has coroutines and exceptions though.

On the negative side a lot of its abstractions are very slightly leaky.

Yes, not too long ago I noted code writing code would help some problems, so this metaprogamming and homoiconicity sub-topic is one I care about. In particular, I want something similar to what you want:

I want languages that have libraries to help you analyze code, transform it, specialize it, optimize it...

Such libraries would have been inhibited in the past by platform dependencies on where code is located and how it is accessed, specifically the file system when all code versions cannot fit in memory. (And even if you could fit every incremental rewrite in memory, you still need to output somewhere.) That's one reason I like the idea of a language knowing about an abstract file system (afs, or VFS virtual file system), so abstract storage manipulations can be written in portable form, only needing a platform specific mapping in each particular concrete implementation. It's weird when a PL delegates part of its semantics to however the OS file system happens to work.

In the mid 90's you would just run out of resources, like RAM, trying to virtualize where everything was stored in a moderate sized code project. Now it's not a problem at all, as long as you work in a low level language like C for the basic infrastructure. Using suitable path conventions in a tree-structured space, you can present code before and after analysis, transformation, specialization, etc., as located in different sub-spaces, then populate things on demand when needed, or access old persistent verions. When an abstract FS lives across sessions, you can do long-lived code versioning with early and later versions both reachable at once, and perhaps used by different processes.

My focus is mainly having both sync and async verions of the same codebase, at different paths, where one derives from the other via continuation passing style, plus binding to a specific process model. I want to write general algorithms in high level style in Lisp, then translate to C, then rewrite that in as many variants as needed, sometimes dynamically when debugging. (I wish that last version had been rewritten to instrument this stuff ... okay let's do that and debug the new process linking that version of code.) I want to keep all the intermediary results, showing the work, instead of just having one original source code and one magic executable at the end. Part of the point is to lower the activation cost needed to move some small thing sideways and try it out, without interfering with other stable versions.

I was thinking of McCarthy's HOPL paper, which would be his memories in 1978 of the thinking that went into the design of Lisp leading up to Lisp 1. Worth rereading; pdf. I see he does mention proving things about programs and in that regard, pure Lisp. The passage I'd in mind would be just after that:

Another way to show that LISP was neater than Turing machines was to write a universal LISP function and show that it is briefer and more comprehensible than the description of a universal Turing machine. [...] Writing eval required inventing a notation representing LISP functions as LISP data, and such a notation was devised for the purposes of the paper with no thought that it would be used to express LISP programs in practice. [...]

S.R. Russell noticed that eval could serve as an interpreter for LISP, promptly hand coded it, and we now had a programming language with an interpreter.

Also relevant to the current discussion is a bit hidden in the last ellipsis there:

D.M.R. Park pointed out that LABEL was logically unnecessary since the result could be achieved using only LAMBDA - by a construction analogous to Church's Y-operator, albeit in a more complicated way.

That's an excellent resource.

Typing adds very little to algorithms.

Do CS people ever think about the core of an algorithm and ask "what's the notation that can express an algorithm in the smallest possible form?"

Not make proofs about it, just express it.

Because that comes close corresponding to what's important to people. The shorter a program is, often the easier it is to understand.

Typing adds cruft that doesn't get you to your answer. And no I'm not saying that lambda calculus that has nothing but closures is enough, I'm saying that you don't need to name types or specify them very often. You can have tuples and lists and arrays and numbers etc.

after Andrey Kolmogorov.

I find fixpoint combinators quite useful in contexts where I want streamable code - e.g. a stream of low level commands for teleoperation, occasionally sending a short loop. There are simplicity advantages, too, e.g. with fixpoints we can use a simple macro expansion layer as an alternative to a full linker. And it's a lot easier to extract and reuse code that isn't entangled with a namespace. Avoiding named recursion isn't just about proofs. There is operational utility, at least for some domains.

alternative to a full linker"

I don't understand what you said here. Can you give an example and explanation?

A typical example for name-based recursion:

factorial n =  
  if (n < 1) then 1 else 
  n * factorial (n - 1)

Here, the definition of factorial contains the name 'factorial' which is bound using an external semantics and operational model for namespaces. This code becomes entangled with the namespace. You cannot trivially eliminate the namespace, e.g. by naive expansion of each word into its definition. Attempting to do so:

factorial n =  
 if (n < 1) then 1 else 
 n * 
   factorial (n - 1)

factorial n =  
 if (n < 1) then 1 else 
 n * 
   if ((n - 1) < 1) then 1 else 
   (n - 1) * 
     factorial ((n - 1) - 1)

factorial n =  
 if (n < 1) then 1 else
 n * 
   if ((n - 1) < 1) then 1 else
   (n - 1) *
     if (((n - 1) - 1) < 1) then 1 else
     ((n - 1) - 1) * 
       factorial (((n - 1) - 1) - 1) 

...

Obviously, any such effort, performed statically, would be divergent. Thus, the burden of managing names and binding becomes deeply entrenched in our runtime operational model. Namespaces might be reified as runtime 'environments'. Fixpoint combinators can avoid this issue.

fix = λf.(λx.f (λv.((x x) v))) (λx.f (λv.((x x) v)))
primRec = λplus.λzero.(fix λr.λn.(if (n < 1) then zero else plus n (r (n - 1))))
factorial = primRec (*) 1

Every place a toplevel symbol is used, we can statically replace that symbol by its definition. In the operational model, this namespace containing 'factorial' and 'fix' essentially becomes a macro expansion layer. Of course, for cache friendly operation you'll still want to limit expansion and reuse compiled subprograms. But even there the clean staging is a simplifying aspect. Cache friendly compilation becomes a separable concern because it's no longer strongly entangled with namespaces or linkers.

More important to me is the ability to eliminate the namespace or treat it as a separate stage. This is convenient for a lot of domains where one might benefit from mobile code, streaming code, or dynamically generated code. Attempting to manage remote or time-varying namespaces is stateful, awkward, and (usually) buggy.

so you maximally expand every named function in place, recursively?

uh

and you call this a "namespace" problem and an alternate to linking...

uh

"Doctor it hurts when I do this"

"Don't do that"

All I can say is that it takes a mathematician to even think of something that naive as a solution to linking and optimization. The amazing thing is that your solution works.

Well it works until you try specializing it for constants, and take the parameters to your y-combinator as constants. Then you're back where you started.

so you maximally expand every named function in place, recursively?

Due to cache-friendly compilation issues, if you do maximally expand everything in place, you'll eventually need to apply a compression scheme to reduce common subprograms. Though, that isn't a bad way to go. It can be useful to expand everything, optimize as far as possible, then find common subprograms that aren't aligned with how the programmer thinks about it, but instead with how the optimizer thinks about it.

All I can say is that it takes a mathematician to even think of something that naive as a solution to linking and optimization.

This isn't really about optimization. It's primarily about having a simple model for mobile and streaming code and generated code, contexts where maintaining a namespace is awkward. ("Doctor, it hurts when I combine namespaces with streaming code." "Don't do that.")

And I'm a programmer, not a mathematician. Many programmers do favor simple solutions because they're less likely to be buggy or to interfere with other features. I've been burned by enough compiler bugs and feature interactions that I have trust issues with any language feature that isn't simple.

Well it works until you try specializing it for constants, and take the parameters to your y-combinator as constants. Then you're back where you started.

I used a Z combinator above. So it isn't a problem to specialize for a constant function. If you have both a constant function and a constant argument, I suppose you could evaluate the whole expression at compile time to its final result. (Modulo divergent loops, of course.) I actually use a variant on the Z combinator that contains 'f' only once, rather than twice, to avoid doubling the serialization cost of the partially applied (or curried) form. I haven't translated the variation I use to lambda calculus, though it should be straightforward.

If you perform full beta reduction in an optimizer, you will need to carefully handle expansion of loops. I think it's fine if the optimizer needs to be careful when unrolling loops. That isn't really a change from where we were before. Unlike namespace or linker layers, the optimizer is intimately concerned with evaluation semantics. I don't believe it's accurate to say that "you're back where you started".

1) because it's the tar-pit that's eating LTU
2) because I don't know anything about it
Do you hear a "but" coming? There's a "but" coming.

"The problem with proving software correct is that maybe Godel blew up that idea a priori."

I don't have a great impression of Godel's achievement even not really understanding it. What I can see is the reactions it got - people were way too impressed with how sweeping it sounded and so instead of subjecting it to mathematical rigor and changing their definitions until Godel's proof no longer attacks mathematics but just says something limited and useful, they just kept huffing the title like it was gasoline fumes to get high off of. Deep, man!

So you start with the assumption that propositions have to be true or false and provable and that blew up in your face... so break it down and turn it into something useful. Also don't break it down in a way that just confuses you until you are no longer capable of asking questions that lead to your paradox. If you say "hey, I've invented a notation so limited that I can't ask any problematic questions in it" that doesn't sound like much of an improvement. It would be better to understand how things go bad. No one threw away division just because it isn't defined at zero. No one threw away zero either. No one threw away subtraction just because you can write 3-7...

What are you trying to get done? :-) Sometimes people like to talk about things because the vein of exploration is fun, not because the goal is reachable. When goals inhabit an abstract philosophical space, they move around a lot. (Smart guy pops back into a room, after a jaunt to alternate dimension, but now he has a facial tic. Cracking a faint grin he notes, "Wow, all your furniture holds still, I forgot how nice that was.")

Proving software correct requires too much perfection. But types can be used to tighten up tolerances in specs so misfit parts show themselves earlier, especially when folks tweak large bodies of existing code, playing with fire. It helps to be told whether round pegs are going in round holes, even if you aren't being warned a peg is made of wood when it needs to be steel.

The practical idea of tolerance, as in parts in mechanical engineering, is useful engineering but it's fuzzy. It's tempting to hope digital tolerances need not be fuzzy as well, because the possibility of perfection seems present, even when it's not because change is also ever present.

Well. Don't worry about not understanding Godel's incompleteness results because there are really not a lot of people in this world who do understand it. You're in good company. It's a bit like 'understanding' QM.

I personally don't even understand that he simply hasn't proven inconsistency instead of incompleteness.

I am bored and things are slow on LtU. So, I am going to ask that thing: That thing that bugs me about Gödel. From the Wikipedia page [1]:

"If p were provable, then Bew(G(p)) would be provable, as argued above. But p asserts the negation of Bew(G(p)). Thus the system would be inconsistent, proving both a statement and its negation. This contradiction shows that p cannot be provable."

Why? Why not simply stop before the 'This'-sentence and simply conclude that the system is inconsistent?

No idea.

[1] http://en.wikipedia.org/wiki/G%C3%B6del's_incompleteness_theorems

The contrapositive of the implication (P provable implies inconsistent) is (consistent implies P not provable). In other words, that final italicized conclusion is assuming the system is consistent. Does that help?

Why not simply drop the assumption that the system is consistent and write it like this:

"If p were provable, then Bew(G(p)) would be provable, as argued above. But p asserts the negation of Bew(G(p)). Thus the system is inconsistent, proving both a statement and its negation."

Isn't it a bit odd to derive unprovability since otherwise the system is inconsistent? I see no reason to assume the system is consistent?

The first incompleteness theorem states that a system cannot be both consistent and complete. This is equivalent to the implication (consistent implies incomplete). Your quote gives the proof (consistent implies p not provable). Wikipedia also includes the other half, (consistent implies (not p) not provable). Combining these two gives the theorem, as incompleteness means that there is some p, such that neither p nor (not p) is provable.

But I can simply drop everything about completeness, drop the whole definition even, assume that systems are either consistent, or not, and simply interpret that Godel derived an inconsistency in an inconsistent system.

Much more direct, if you ask me.

But isn't completeness the whole point? I'm not sure I get what you're driving at here. What's the point of the interpretation "inconsistent systems are inconsistent"? This would seem to have no information content. Is it that, if this is "all" Gödel showed, then we don't need to feel uncomfortable or worried about the result?

In order to get out of inconsistency of math, Godel introduced the notion of incompleteness, and subsequently proves that unprovable sentences must exist.

What if I don't try to get out of inconsistency with a definition of incompleteness but simply go back pre-Godel, drop the notion of completeness, and assume systems are either consistent or not?

I simply don't see what's wrong with an interpretation that he has proven (logic over) arithmetic inconsistent. As in: maybe the quantifiers are wrong, or something else.

Maybe we should all be finitists?

Pre-Gödel, it was hoped that it may be possible to formalize mathematics in a way that was complete; i.e., that for every P, either P or its negation is provable. Gödel showed that this is not possible. That is, we had to "drop the notion of completeness". I wouldn't phrase it as Gödel introducing some new notion called incompleteness. Rather, he showed that this old notion called "completeness" was doomed to failure, and had to be given up. I don't see a difference in the result from what you suggest: drop the notion of completeness, and assume systems are either consistent or not. (This latter point resting on the law of excluded middle).

Some focus on logics where where maybe everything can be proven mechanically, I suppose.

The idea that mathematics should be founded on a set of axioms — and thus, that everything that's true should follow from those axioms, completeness — was less than a hundred years old when Gödel came out with his Theorems. Math had always been based on intuition, and there was a crisis going on in mathematical foundations in the early nineteenth century because they'd been obliged to swallow complex numbers and had indigestion; trying to justify complex numbers using intuition was not working well, the closest they came was the geometric interpretation of complex arithmetic in the Gaussian plane. Folks were looking for some kind of number that would have a 3D goemetric interpretation, because they really, really wanted to be able to treat a directed magnitude in physics as a "number", and when Hamilton came up with numbers that were like that (quaternions) using an axiomatic approach, the axiomatic approach gained hugely in credibility. Anyway, the point is that the expectation of completeness was a fairly recent thing when Gödel's Theorems appeared; you might even date it from Frege's work, in which it was about as old then as Lisp is now.

This is a response to your final parenthetical question, and a last attempt to help clarify things, which I think I've so far failed to do.

The structure of the proof is to derive a contradiction from the assumption of the provability of P (and also, of not P). "Provability" is a key assumption, because the code of the proof of P is a necessary ingredient to derive the contradiction. So we can't "simply stop" before mentioning provability; it's what gets us off the ground.

Two assumptions lead to the contradiction. We assumed consistency and we also assumed that we had a proof derivation for P in hand. It's not logically sound to say the first assumption, consistency, is definitely the wrong one. ("We've proved inconsistency. Let's stop here.") We are also forced, out of logical necessity, to consider the possibility that, perhaps we didn't have the proof code for P in hand after all.

[EDIT: Ah. Forget it. That didn't make much sense.]

Gödel's results are invalid because he made use of a "self-referential" proposition that leads to inconsistency in mathematics. Using computational undecidability of the halting problem, Church/Turing provided a valid proof of inferential incompleteness of the Peano/Dedekind theory of natural numbers.

See page 14 of Inconsistency Robustness in Foundations.

To try to be a little more helpful: it would be fine to leave that first implication as (P provable implies inconsistent), since, combining with (not P provable implies inconsistent) gives the main theorem in the form (complete implies inconsistent). This would be logically equivalent to the argument Wikipedia gave (at least with classical logic).

Wittgenstein showed that Gödel's "self-referential" proposition leads to inconsistency in mathematics:

Let us suppose I prove  the improvability (in Russell’s system) of P
[i.e., Suppose ⊢⊬P where P is Gödel's “self-referential” proposition "I am not provable." so that P⇔⊬P] 
then by this proof I have proved P [i.e., ⊢P].
    Now if this proof were one in Russell’s system [i.e., ⊢⊢P]—
I should in this case have proved at once that it belonged [i.e., ⊢P] and
did not belong [i.e., ⊢¬P because ¬P⇔⊢P] to Russell’s system.
    But there is a contradiction here! [i.e., ⊢P and ⊢¬P]

See page 7 of Inconsistency Robustness in Foundations.

My understanding of your reading of that quotation (I'm not concerned with Wittgenstein's intention) is that it proves this:

(*) From PM ⊢ ¬"PM ⊢ P", which is equivalent to PM ⊢ P, it follows that PM ⊢ ¬P. In other words, supposing PM ⊢ ¬"PM ⊢ P", it follows that PM is inconsistent.

I'm using PM for Principia Mathematica (i.e., Russell's system) and "PM ⊢ Q" (quotation marks included) as shorthand for Prov(#Q).

So far, so good. This is just a restatement of part of Gödel's proof. Now, if PM is consistent, then it follows that our supposition, which was equivalent to PM ⊢ P, must have been wrong. So didn't we just prove PM ⊢ ¬"PM ⊢ P" ?! I.e., didn't we just prove our supposition, so that the conclusion of inconsistency necessarily follows? No, we did not show that ¬"PM ⊢ P" follows from the rules of PM. At the very least, we'd need to include our assumption that PM is consistent in the context, to get something like

PM ⊢ (¬"PM ⊢ ⊥" → ¬"PM ⊢ P").

This leads in, of course, to the second theorem ...

It's possible I've misread your reading, and ultimately it was my guess as to what the "inconsistency in mathematics" could refer to, as it wasn't explicitly spelled out. I assumed, in particular, that it had to mean more than just (*), as otherwise you're just agreeing with Gödel.

I briefly looked at consistent and complete arithmetic. Informally, I suppose I can abbreviate that as: when adding things consistent and complete logics exist, once you start multiplying it ends.

Is there some informal easily grokkable reason why this is? Or did I get it wrong?

I think I got it.

By the proof that I quoted above, Wittgenstein showed ⊢P and ⊢¬P where P is Gödel's "self-referential" proposition.

Ok. This confirms that your reading was what I thought it was.

Was that all you sought to accomplish with this response?

The original comment of yours I replied to made a strong claim. I presumed your intent in posting was to convince others of this claim. My response to you was offered in the spirit of helping you with this goal: I took pains to carefully spell out the understanding I came to of what you said, and also to carefully explain exactly why I was not convinced. This is so that you can change my mind! Point out where I misunderstood, where my attempt to be precise didn't match your intent, where I took a step of logic that wasn't valid.

Your reply was fine; it did give me a small piece of information about what you think. But, surely you couldn't have thought it would do anything to help convince me? Do you care about convincing anyone? I'm just one person, and I'm no expert; there's no need to engage me or my analysis. But you don't seem to engage anyone else, either.

There's a glaring missing reasoning step here. How do you get from "Suppose X, then ⊢P and ⊢¬P" to "⊢P and ⊢¬P"? I proposed one possibility, but also showed that it was an error. What's your alternative?

Hi James!

I was responding to your question "What is the contradiction?".

Summarizing Wittgenstein:

If we suppose Gödel's 1st incompleteness result is provable
(i.e., suppose ⊢⊬P where P is Gödel's “self-referential” proposition), then
there is a contradiction.

Regards,
Carl

Notice that this summary is quite different than the one in your previous comment. It's important to be precise! Your new summary still looks inaccurate, for what it's worth.

The understanding I came to, and carefully laid out in my first reply to you, remains intact. I'm not being obstinate here. This latest version of your assertion is more or less what I suspected you thought in the first place, and what I responded to.

Shall we leave it at that? Now that my replies have hit 0 technical content, I don't see the point of continuing, on my side. You could always engage me on the substance of my initial reply...

James,

My summary accurately summarizes the structure of Wittgenstein's argument from the box in my post.

Unfortunately, the notation that you used in your post is not the best :-(
Your best bet may be to abandon this notation and go over to something more modern.

I will be happy to respond to any questions that my have about modern more precise notation.

Regards,
Carl

Get back to me with a working computer implementation of Classical Direct Logic, so that I can write proofs and have the computer verify them. Then I'll implement the first incompleteness theorem for you. I don't think anything else would satisfy us both as to using "modern notation" and as to being "precise."

I am not confused. I have no questions for you. I challenged you to convince me, and gave you all the help I could to do so. Obviously, I remain unconvinced. If you can point to something specific in my notation that was not precise or was not modern, I'd be happy to clarify.

Classical Direct Logic clearly proves Gödel's 1st incompleteness theorem for ℕ using the proof of Church/Turing. See page 14 of Inconsistency Robustness in Foundations.

However, Gödel's 2nd incompleteness result is false because Mathematics proves its own consistency :-)

Right, you won't be surprised that the theorem is provable. But the point is I would implement Gödel's proof. Not that I think if you saw a computer-verified version of Gödel's proof using your own system, you'd give up your claim that it is invalid.

"If p were provable, then Bew(G(p)) would be provable, as argued above. But p asserts the negation of Bew(G(p)). Thus the system would be inconsistent, proving both a statement and its negation. This contradiction shows that p cannot be provable."

Why? Why not simply stop before the 'This'-sentence and simply conclude that the system is inconsistent?

Abbreviating that quote: "If p were provable, then [the system would be inconsistent]." We can't just upgrade that to "the system is inconsistent" without justification. (If for some reason we knew p were provable, that would be justification.)

In my view, he simply needs to show his logic consistent first. [found the bug in my reasoning, I read the Wikipedia page argument wrong.]

Needs to show which logic consistent first? His meta-logic?

Probably both. I wouldn't know. Honestly, I just read Godel's argument superficially. And somehow I took the contradiction constructively; i.e., as a procedure of turning a provable into an unprovable, I guess.

But it's all very superficial reasoning where I liberally 'erase' the encodings.

It all made a lot more sense to me (and somebody around here was pointing me to where somebody else had done the same earlier) to cast Gödel's results in terms of Turing machines, making it possible to do a proof that's scarcely more complicated than the routine proof that the halting problem is undecidable. I worked it all out in the form of a blog post.

I wouldn't know if you can look at Godel through the eyes of Turing machines, to be honest. Guess I should buy GEB, it's all a long time ago.

Thing is, I can read Godel's argument and superficially agree with it too.

Too sloppy I guess.

When I wrote my dissertation, I extracted this overview of the proof:

For sufficiently powerful M, one can construct a proposition A of M that amounts to "this proposition is unprovable". If A is proven, that would show that A is false, thus would constitute a proof of not-A; if not-A is proven, that would constitute a proof of A; so if M is consistent, both A and not-A are unprovable. (This is Gödel’s Theorem, that M must be either incomplete or inconsistent.) But then, a proof that M is consistent would constitute proof that A and not-A are unprovable; and a proof that "A is unprovable" is a proof of A, and a proof of A means that M is inconsistent.

What's unsatisfying about this, to me, is that it doesn't explain how proposition A is supposed to "amount to" this-proposition-is-unprovable, and I was motivated to write a proof where the only details omitted are unimportant tedium, rather than key points like that. It's important to make clear that there is no explicit self-reference involved; it's just that there must be some arithmetic function, which the logic M can consider statements about, that behaves identically to M.

There are three constructive procedures in the proof (of Rosser's version). The procedure for producing the sentence P, given the object system, is constructive. Then there is a constructive procedure taking as input a proof of P, producing a proof of not P. In Rosser's version, there is a constructive procedure going the other direction, taking a proof of not P and producing a proof of P. We have all this without assuming consistency. Note, you refer to an additional "assumption" of possible incompleteness, but this is an absence of an assumption (of completeness); it doesn't require assuming anything. The only conclusion we can draw at this point is that, if we could ever find inputs for the last two procedures, we would then know for sure that the object system is inconsistent. The detail that the final two procedures operate on proofs and not on sentences/propositions is a rather critical one. If you want to say, the object system is either consistent or it isn't, this is an extra step. The case of inconsistency is not very interesting, as the object system then proves all sentences. Nothing has been done to rule out the other case, that of consistency. We haven't constructed an inconsistency yet, not without an input to one of the last two procedures.

I guess a proof of inconsistency of the object logic would render the meta logic inconsistent, as well. And Godel would have proven nothing.

Nah. I found it. It's the wording of the wikipedia page. It reads somewhat like "we found a contradiction, that cannot be, therefore we go over to concluding unprovability" whereas they mean "assume something, contradiction, therefore not something. Repeat for reverse case. Unprovable."

Got it.

By "prove the improvability of P," Wittgenstein meant ⊢⊬P.

Wittgenstein argument was that assuming Godel's result ⊢⊬"I am not provable." leads to inconsistency in mathematics.

I wouldn't worry too much about it. Hewitt's claims are extraordinary, which, as the saying goes, calls for extraordinary evidence; extraordinary evidence has failed to emerge, despite whatever Hewitt or others here (including me for years, until recently) have done. Until and unless it does emerge, this stuff won't be useful for implementation or theory.

John,

It is necessary to read and understand an article in order to properly critique it ;-)

Regards,
Carl

A language whose computations always terminate (and therefore has no general recursion or Y combinator) is useful because the type tells us that we *will* get a value--not only that we might. When using the type system as a logic, if we could reach arbitrary conclusions (types) by going into infinite loops, the logic would be unsound.

When there's no general recursion (or any other chance of nontermination), it's called total functional programming. That is, the functions are total functions, not partial ones. We can see this in Coq, Agda, Epigram, and Idris. Agda and Idris are particularly notable for being designed for programming, as opposed to Coq's theorem-proving focus.

I think Idris has effect types and syntactic sugars so that it's easy to switch between a verifiable total FP style and a flexible ML-like style for different parts of a program.

(Anyway, this is a thread started by Hewitt, so it's probably going to involve extraordinary claims at some point. Total FP is already a pretty hard sell if you're not already trying to do program verification using a type system.)

I understand the restriction of general recursion and how termination can be guaranteed by things like structural recursion, for example languages like Epigram.

This sounds like something different, but it could just be that it is not being explained very well.

Procedures in ActorScript can be partial. For example Factorial.[0] does not converge using the following definition:

Factorial.[n:Integer]:Integer ≡
 n=1 � True ⦂ 1
        False ⦂ n*Factorial.[n–1]

Why doesn't that lead to logical inconsistencies?

Total mathematical functions are different from executable procedures with a different notation:
* Total mathematical function f:Boolean^ℕ so that f[3] is either True or False
* Potentially partial procedure g:NaturalNumber↦Boolean so that g.[3] might diverge

Just something like "don't write loops unless you can prove that they will end?"

Is there something horrible hiding in there like "force a type system on people that makes it hard to write loops?"

You know, it's impossible to define a loop in SQL, so there's long been a place for limited languages, but I wouldn't want to write an application in one.

Ask him how he would implement a REPL in his ideal language. One that loops till the user asks it to end.

Actually he said my definition of the y-combinator was wrong (it's not but it is the lazy version, so it was the wrong one for an eager language), he did not say it would be rejected. Although on re-reading the choice of the word "erroneous" is a bad one, as it is ambiguous as to whether the definition is a valid definition (but not the Y-combinator) or that it is an invalid definition.

When he says "fixed points considered harmful" is he talking about flow of control, ie, just looping?

I agree types are fundamental, and I also prefer strongly typed languages. However other type systems admit fixed-points, so to say "types mean that fixed points do not exist" is clearly wrong. So what do you mean? How does your type system differ from other type systems such that fixed-points cannot exist? Surely if you allow general recursion fixed points do exist (even if not explicit).

The universal type does not exist.

Consequently, there are no fixed points.

Hold on, as most type systems do not have a universal type (a '*' or anything type) it sounds like you are talking about the universal quatifier. Does that mean you cannot write generic algorithms, for example the identity funciton:

id : forall a . a -> a

Is really useful, but the next simplest generic function is also useful:

swap : forall a, b . (a, b) -> (b, a)

How would you express these functions in ActorScript or DirectLogic?

The following is an identity procedure:

Identity◅aType▻.[x:aType]:aType ≡ x

The following is a swap procedure:

Swap◅aType, anotherType▻.[x:aType, y:anotherType]:[anotherType,aType] ≡ [y,x]

Isn't the universal quantification implicit?

forall a . Itentity<a>.[x:a]:a = x
forall a, b . Swap<a, b>.[x:a, y:b]:[b, a] = [y, x]

How about:

Y<a>[f:[a]->a]:a = f.[Y.[f]]

In eager languages you need to think about the order of evaluation when using a fixed point, otherwise it'll just unwrap the definition of Y an infinite number of times. By making an extra argument explicit you can make sure you get a fixed point operator with the right semantics.

let rec fix f x = f (fix f) x (* note the extra x; here fix f = \x-> f (fix f) x *)
 
let factabs fact = function   (* factabs has extra level of lambda abstraction *)
   0 -> 1
 | x -> x * fact (x-1)
 
let _ = (fix factabs) 5 

I imagine ActorScript is eager, therefore, at minimum, he needs to supply an extra argument. But then, I gather, his typesystem blocks the definition.

Sorry, too much Haskell. I prefer eager though. I am trying to understand how it blocks the definition.

Roughly, you need to think in the operational model of both languages, which can be thought of as evaluating thunks (stack frames in the heap.)

If you have

fix f = f (fix f)

then an application gets rewritten eagerly like

fix f x
= f (fix x) x
= f (f (fix f)) x
= ...

Because fix is a unary function, it's a function argument with all parameters supplied, and eager evaluation enforces the evaluation of arguments.

If you have

fix f x = f (fix f) x

then

fix f x 
= f (fix f) x (* fix f cannot be rewritten since it lacks an argument *)
= ...         (* f is rewritten *)

And fix f cannot be rewritten since it lacks an argument. It's a curried application, is pushed as a thunk to the heap, and f is evaluated.

(Guess I overdid delayed evaluation in my own definition. I'll look at it once.)

Ah. I do it a bit differently in Hi.

 fix = [ f -> f [x -> (fix f) x] ]

Then

fix f x
= [ f -> f [x -> (fix f) x] ] f x
= f [x -> (fix f) x] x
= .. (* f gets rewritten since the argument is a lambda term *)

You can pick either. Guess the ML one is neater but that Wikipedia page didn't exist when I needed my own eager fixed points.

Are you still working on Hi? Your profile reference to www.hi-language.org has been broken for a long time.

A Z-combinator (eager) fixpoint can also be expressed using types, too.

fix :: ((a→b)→a→b) → (a→b)
fix f = f (fix f)
-- is equivalent to
fix f a = f (fix f) a

In any case, depending on the namespace to tie the knot here seems like cheating to me. You're essentially using the namespace as an implicit fixpoint. You aren't really implementing fixpoint, you're just leveraging one that the compiler implements. This would be obvious if you were to model the namespace explicitly.

The only difference is whether you define Y as a unary of dyadic combinator. If you define it as a dyadic combinator, you can rely on (some languages) operational semantics that 'fix f' simply will not be expanded but evaluation will be deferred until fix receives two arguments.

Namespaces have nothing to do with it?

Yah. After a five year break I decided to implement a Hi interpreter/compiler in C++ since the bootstrap failed to deliver performance. (It's one of those nasty features of bootstrapping, you only can measure performance after you went through the whole process.)

I was roughly three orders, 1000x, off of what I think I would need to deliver an acceptable tool. Fixing the bootstrap would require a similar effort like for Haskell/ML; i.e., a twenty to hundred manyears which I don't have.

So I decided to write an interpreter/compiler in C++. Fast interpreter, slow language. I'll hopefully end up with something like Python/Mathematica speed.

But it's tedious and I often don't really feel like since I already went through the whole process once.

My blog has some information on it.

Typically 'namespace' is used in context of distinguishing many namespaces, e.g. `math:tan` vs. `color:tan`. But the difference between zero and one namespace is more interesting. Many languages, such as lambda calculus, don't have even one namespace.

With `fix f = f (fix f)` you're relying on a fixpoint in the space of named functions to bind the 'fix' on the LHS to the 'fix' on the RHS. The fixpoint behavior is pushed up to your compiler or linker, which cannot naively inline the definition in place of every symbol. (In this sense, the namespace becomes relevant to the operational model.)

You could express fixpoint without relying on the namespace, but it would typically be more verbose. E.g. `Z = λf.(λx.f (λv.((x x) v))) (λx.f (λv.((x x) v)))` in lambda calculus.

I'll check out your blog on Hi language. Thanks.

The blog is more of a log which I use to order my thoughts sometimes as well as log what I was thinking about at what point during the development.

On second thought, forget about the blog. It's not informative enough and the language didn't change. There's a working link with a bootstrap (don't download it) and some pdf's on the language if you're wondering about what this small declarative language is about.

But I doubt I'll ever find a lot of users. Haskell/ML have evolved far beyond what is reachable for me, and I am not sure the combination pure/eager is even what people want. People want to write for loops in scripting languages.

The language will probably remain an oddity unless I can find some use-case for it.

If I define:

Itentity<a>.[x:a]:a = x
Swap<a, b>.[x:a, y:b]:[b, a] = [y, x]

Are the 'a's different? If they are then they must be introduced with an implicit universal quantifier, like in Prolog clauses.

Sure, lets use the eager variant then:

Y<a>.[f:[[a]->a]->[a]->a)]:[a]->a = f.[Y.[f]].[x]

Postponing execution doesn't help implement the Y combinator in ActorScript because the following is not the definition of the Y combinator [edited for clarification]:

  
Y◅aType▻.[f:([aType]↦aType)]:aType ≡ postpone f.[postpone Y.[f]]

What do you mean incorrect. They Y-combinator is not incorrect because it exists, and the Haskell version of that code works fine:

{-# LANGUAGE ScopedTypeVariables #-}

fix (f :: (a -> a) -> a -> a) = \(x :: a) -> (f (fix f) x :: a)

fact f x | x == 0 = 1
fact f x | x /= 0 = x * f (x - 1)

Is there an ActorScript interpreter that I can use?

Can you explain to me why the above definition of the Y combinator would not work. What would the type error message be?

Why is that type not:

x : ([SingleArgument<aType>]->SingleArgument<aType>)

Also I don't see what is wrong with this definition:

Y<a>.[f:[[a]->a]->[a]->a)]:[a]->a = (f.[Y.[f]]).[x]

Y combinator is far from the only fixpoint combinator. Can you prove ActorScript expresses none of them? As I understand it, ActorScript is Turing complete. If so, you certainly can model within ActorScript a language where you can express a fixpoint combinator and an interpreter for it.

Partial functions exhibit the same 'considered harmful' problems you ascribed to fixpoints. So I'm not understanding why your attack focuses on fixpoint combinators in particular, much less the Y combinator even more specifically.

I know of only one logic in which proof-by-failed-attempt might be considered valid. It's a very inconsistency robust logic, too. But, for various reasons, durnken logic doesn't get much respect from the academic community.

It can be proved that no implementation of Fix can be expressed in ActorScript.

But a formal proof can be tedious :-(
The basic idea is that every ActorScript type has finite rank but an implementation of Fix requires a type that is not of finite rank.

But the proof is tedious :-(

Yeah, right. At every turn you provide an excuse for avoiding clarity and rigor.

Now tell me again to go ask a specific question about the N+1th version of this or that paper.

SingleArgument◅aType▻ ≡ [aType]↦aType

Fix◅aType▻.[f:([SingleArgument◅aType▻]↦SingleArgument◅aType▻)]:SingleArgument◅aType▻ ≡
 [x:aType]↦(f.[Fix.[f]]).[x]

I'm still wondering about this fixpoint definition in particular. Doesn't this work?

Several attempts by Keean Schupke, marco, and dmbarbour elsewhere in this thread have had simple flaws, such as forgetting to introduce the variable x before using it. Maybe my definition has a flaw too, but I don't see it yet.

(This came up again when I mentioned my lingering doubt in this thread.)

Hey! My fixpoint combinators are purrfect!

Yeah. :) I don't see anything wrong with them except that they're not in ActorScript notation. I had assumed Hewitt was ignoring them on that basis.

Apparently my writing in ActorScript notation didn't make much difference, so I don't know anymore!

I'm still wondering about this fixpoint definition in particular. Doesn't this work?

I don't think so. How would you reconcile it (to create a Goedel fixpoint sentence) with the rules for constructing sentences at the bottom of page 27. The one that begins "x:Sentence ⇔ x constructed by the rules below:"

Drat, I got the lambda syntax wrong. The syntax []↦ is for executable procedure types, and the syntax []→ is for executable procedure lambdas. I also wrote Fix.[f] when perhaps I should have written Fix◅aType▻.[f]. Here's an update:

SingleArgument◅aType▻ ≡ [aType]↦aType

Fix◅aType▻.[f:([SingleArgument◅aType▻]↦SingleArgument◅aType▻)]:SingleArgument◅aType▻ ≡
 [x:aType]→ (f.[Fix◅aType▻.[f]]).[x]

Now for something else you're saying...

to create a Goedel fixpoint sentence

In this subthread, I'm not talking about fixed points for sentences, nor of fixed points for ActorScript's total mathematical functions. I'm just talking about fixed points for ActorScript's partial executable procedures.

Hewitt gave an example of a recursive partial procedure Factorial, so it seems like even if this combinator exists, it won't cause any emergence emergency.

However, Hewitt specifically argued that this fixed point operator did not exist, with an argument based on showing a failed implementation attempt. My reply offers an implementation with the same type signature as that attempt. Hewitt responded by objecting to a slight (broken) variation. (The variation uses x without even establishing a binding for x first. (EDIT: Hewitt has fixed this.)) Is his remaining objection that my definition doesn't work, that his variation doesn't work, or just that it isn't "the Y combinator" in particular?

Anyway, this stuck in my mind because it's a good example of why I'm suspicious of Hewitt's arguments of the form "The missing type ⍰ does not exist." As (hopefully) constructive advice for Hewitt, I think the proofs that use this technique need to be rewritten... or at least elaborated upon to explain why the failed attempt is the only attempt that could have worked.

This is an excellent question :-)

Direct Logic uses typed recursion instead of the Y combinator.
It is easy to prove that using typed recursion in Direct Logic, every type has finite rank.

The claim is that fixed points cannot be defined in Direct Logic because of type constraints, e.g. the definition of the Y combinator does not work in Direct Logic. Unfortunately, I do not have an elementary proof of the claim ready to hand :-(
However, you may be able to construct one or find one in the literature :-)

Edit: Also, it is possible to give a signature for Fix◅aType▻ (but not an implementation) so that Fix◅Sentence▻ doesn't create a "self-referential" sentence.

This is an excellent question :-)

And that's an informative response, thanks!

I know that in the simply typed lambda calculus, fixed point combinators don't exist because every type has finite rank. I had assumed the Foo◅aType▻ brackets were something like ML-style polymorphism, which would have made this combinator possible. However, I can imagine at least one variation that wouldn't support fixed points, and that's if every occurrence of Foo◅aType▻ were automatically replaced with its definition (much like Lisp macroexpansion).

I'm not sure if that will give me the proper intuition of how this works in your system, but it gets me unstuck, I guess. :)

It's extremely interesting to think that this is a system with a sort of graph-like scoping policy for recursive executable procedures, but also strict types (reminiscent of total FP) that happen to prohibit a fixed point combinator.

David was talking about how most implementations of fixed point combinators rely on the recursive nature of the namespacing mechanism, and how he prefers using fixed points directly. It looks like ActorScript decisively commits to recursion-by-namespacing, drawing a correspondence between interacting Actors and interacting definitions. (I hope I'm not again seeing something that isn't actually there....)

Thanks!

Types have raised very subtle issues ever since Russell started his investigations.

Of course, it is not settled that ActorScript and Direct Logic have got types right ;-)

As mentioned at the top of this topic, untyped fixed points can do a lot of damage if they exist.
Consequently, it would be great to have a formal proof that they don't exist in ActorScript and Direct Logic.

PS. Of course, it is easy to prove that fixed points do not exist in the simply-typed lambda calculus.

I have nothing to add to Hewitt's reply to other than I did mistakenly assuming you were trying to define Y for the purpose of trying to create a Direct Logic realization of Goedel's second incompleteness so-called theorem.

so-called theorem

Now you're just trolling.

Gödel's "Second Incompleteness Theorem" has come under serious question as to whether or not it applies to Mathematics.

Consequently, Thomas was legitimately allowed to call it a "so-called theorem".

Note that the Church/Turing theorem of inferential incompleteness of the Peano/Dedekind categorical axiomatization of ℕ still stands.

The claim was that Goedel never worked out his proof. So what. Someone else did, peer reviewed and everything.

Goedel 2nd is understood by some. Not me. But here is Boolos.

Furthermore, you like to troll. I've seen you calling CSP a "programming language" and make other claims which "stimulate discussion".

But personally, that doesn't bother me. You like to take the knives out in a discussion, I don't believe in discussions in hushed tones while walking around lily ponds either.

But my critique remains, on glancing through your papers, things aren't sufficiently pinned down to discuss reasonably.

The problem is not that Gödel didn't present a formal proof. Gödel's "2^nd Incompleteness" writing and subsequent work by others depended crucially on the existence of the Mathematical sentence "I am not provable" alleged constructed using a non-existent fixed point (sometimes called the Diagonal Lemma).
Also, Gödel's "2^nd Incompleteness" so-called theorem has now been contradicted by a theorem of Mathematics.

PS. Communicating Sequential Processes (CSP) was name that Hoare gave to a programming language.
Later he decided to use the same name for something else.
Consequently, the name is now ambiguous.

PPS. Comments and suggestions are greatly appreciated on the articles that you have had a hard time understanding.

Unless you make that precise, I don't understand what you're talking about. I've read the Stanford expose, don't see anything wrong with it, don't have a problem with effective enumerability, don't see problems with a diagonal lemma, don't see explicit self-reference, don't find quoting a big problem, and doubt that types will lead to a weaker logic where the construction is prohibited. (And doubt that the construction of a weaker logic makes a lot of sense; you end up with a weaker logic, but the result still holds.)

To me it only signifies that discrete thought about a continuum is effective, but when turned on itself leads to absurdity. And I find that natural, since I believe in Panta Rhei. So, you're discussing this with the wrong person anyway since I believe most thought is fundamentally flawed anyway.

But I am not trained a logician. Write it down and get it peer reviewed. That's all I can say. Discussing this on LtU is maybe entertaining to some but leads nowhere.

PPS: Historically it is nice to know CSP started out as a programming language. But that's irrelevant. You're just teasing. You know it has been widely successfully used as a formal language.

Goedel 2nd is understood by some. Not me. But here is Boolos.

Boolos does not understand it either, as evidenced by the passage that says:

In fact, if math is not a lot of bunk, then no claim of the form "claim X can't be proved" can be proved.

Boolos means for any fixed sufficiently powerful formal system called "math" and, of course, this is correct.

-

Boolos means for any fixed sufficiently powerful formal system called "math" and, of course, this is correct.

Far from correct, Boolos' claim is trivially either false or "not even false", depending on how you read it.

In DL, as an example, you can prove that you can not prove 2+2=5 very directly. In that sense, Boolos' statement is false.

What we might generously suppose that Boolos means is that even if we can prove the non-provability of 2+2=5, we still have not ruled out the possibility of an inconsistent system (in which we can also prove the provability of 2+2=5).

But that is different. That is saying that you can't rule out that a (sufficiently powerful) system may yet be revealed to be inconsistent.

The ability to prove that you can't prove 2+2=5 does not imply inconsistency (but neither does it rule it out).

To prove that DirectLogic can't prove 2+2=5 means to prove that there is no chain of inference admissible in DirectLogic that leads to the conclusion 2+2=5. Note: this has nothing to do with the presence of unicode symbol U+22A2 in the DirectLogic grammar.

The system of "math" (call it M) Boolos has in mind allows proof by contradiction. Thus if M is inconsistent, then M proves absolutely anything. Conversely, if there's any proposition M does not prove, then M is consistent. If you can prove that "2+2=5" is not provable, then you can prove M consistent.

To prove that DirectLogic can't prove 2+2=5 means to prove that there is no chain of inference admissible in DirectLogic that leads to the conclusion 2+2=5.

That proof is trivial (hence "not dispositive" aka "doesn't put the question to bed") in Direct Logic.

Goedel's 2nd is incorrectly popularly understood to mean that Direct Logic's trivial proof of the unprovability "2+2=5" is impossible in a system that is both consistent and that can contain a model of ℕ.

The catch to the trivial proof is that, who knows, maybe it can also be proved that "2+2=5" is provable in DL. I'm confident it can't but my confidence is empirical. I regard it as a scientific question.

In Goedel's 2nd theorem argument, instead of the naked turnstile ("⊢"), he has a predicate over an encoded model of the subject system, along with an implicit assumption of the derivability axioms.

As it turns out, therefore, Goedel is talking only about a pretty confined class of systems: systems with those axioms and supporting those particular definitions. If a system doesn't have those axioms or doesn't accept those particular definitions, the argument called Goedel's 2nd theorem just does not apply. Period.

The informal error that is popular, that Boolos and you are reiterating, is that the derivability axioms and validity of those definitions is inevitable in a "suitably powerful" fully general foundation of math.

DL gives you a pretty compelling counter-example.

Again, it is not correct to make the meta-level claim that "DirectLogic proves that DirectLogic cannot prove 2+2=5" on the basis that DirectLogic proves "¬ ⊢ 2+2=5". In order to make that claim at meta-level, you must judge at meta-level that "⊢" means provability in DirectLogic. Unfortunately, this meta-level judgement is not sound.

The proof is pretty straightforward, I think: Suppose that we have a model that interprets the naked turnstile as asking for the existence of a certain proof object, encoded as a natural number. Then we can soundly expose the way we're encoding things to the logic. Once we do that we will run afoul of Godel in the ordinary way and our system will be inconsistent, contradicting the assumption that it has a model.

Edit: Oops. That reasoning was sloppy. You might not get into trouble with Godel after all, since by exposing reasoning to the logic, you change the logic. So maybe this is sound. I'll have to think more later.

There is no meta-level in the argument sketched for Goedel's 2nd theorem.

Suppose that we have a model that interprets the naked turnstile as asking for the existence of a certain proof object, encoded as a natural number.

I can't suppose that since it would not be an accurate model of DL.

I think that part was fine. You can always choose numbers to encode your symbols.

But my reasoning was flawed. See my edit if you haven't.

Edit: yeah, the only thing I see about DL that doesn't look sound is that it proves turnstile isn't enumerator. Even if it were possible to interpret it soundly, I don't think it should count as proving consistency unless thats the only interpretation.

Gödel numbers are pretty much irrelevant to inferential incompleteness.
See the Church/Turing proof of the inferential incompleteness of the closed theory ℕ.

Church's Paradox shows that the theorems of Mathematics are not computationally enumerable.
Direct Logic turned Church's argument around into proving the theorem that Mathematics is open, i.e., inexhaustible. :-)

However, there are still grounds for concern that Direct Logic could be inconsistent, regardless of the correct proof that Mathematics is consistent.

The above definition of Fix is not the Y fixed point procedure.

I see what you're saying--that this operator is only able to derive fixpoints that are functions, as opposed to fixpoints of arbitrary type--but the actual Y combinator is almost beside the point.

When Keean Schupke first brought up "the Y-combinator" in this thread, and when marco was saying "Why would I use Actorscript if I can naturally define a Y combinator in most other typed languages?" I think they didn't necessarily need the Y combinator itself. They evidently would be satisfied with the "eager variant," the Z combinator.

Back in this post of yours, you demonstrated a flawed way to assign types to the usual untyped lambda calculus implementation of the Y combinator:

The Y combinator cannot be defined using ActorScript:

 
SingleArgument◅aType▻ ≡ [aType]↦aType

Helper◅aType▻.[f:SingleArgument◅aType▻]:SingleArgument◅aType▻ ≡
                [x:([⍰]↦SingleArgument◅aType▻)]→ f[x.[x]]
 
Fix◅aType▻.[f:([SingleArgument◅aType▻]↦SingleArgument◅aType▻)]:SingleArgument◅aType▻ ≡ 
                (Helper◅aType▻.[f]).[Helper◅aType▻.[f]]

The above attempted definition of the Y combinator does not work because the missing strict type ⍰ does not exist.

The final type signature you used is specific enough that the Z combinator would be a valid implementation, so I think I mistook you for saying Z itself couldn't be defined. Sorry for my contribution to this misconception.

The implementations Keean Schupke, marco, and I gave are pretty standard implementations of Z. Actually, if I were defining Z itself, I'd give it a slightly more relaxed type than the type of Fix above:

Z◅a, b▻.[f:([[a]↦b]↦([a]↦b))]:([a]↦b) ≡
    [x:a]→ (f.[Z◅a, b▻.[f]]).[x]

If combinators like this can be defined and used for constructing recursive functions, even if the actual Y combinator does not have a well-typed definition, I think that'll be a pretty nice clarification.

Omitting types, just looking schematically at the defintion, the Z combinator would be:

  Z.[g] -> [x] -> g.[[v]->x.[x].[v]][[v]->x.[x].[v]]

Immediately, by inspection, we can notice the critical sub-expression:

  x.[x]

Here, "x" is presumptively a function whose domain is the function type itself.

In DL's constructive type theory, a function type can only be formed from domain and codomain of lesser rank. Therefore, "x" has no valid type.

Isn't the lesser rank restriction overly restrictive to avoid paradoxes? Don't you only need the rank to be lesser or equal for non-negated application, and only strictly lesser for negated application (as in datalog's restrictions).

Don't you only need the rank to be lesser or equal for non-negated application, and only strictly lesser for negated application (as in datalog's restrictions).

I don't really know anything about datalog.

By "negated application" do I guess correctly that you are talking about modeling functions as predicates expressing a relation between domain and codomain, and in particular terms which logically negate such a predicate?

In DL and ActorScript logic programming, propositions are sentences of Boolean type. They are all of a single type. Rank of types do not come into question.

Proposition values are ranked, but all those values are the same type.

Surely propositions cannot be Boolean, and inconsistency robust (As Boolean algebra had the law of the excluded middle). I would have thought propositions need to be Heytingean, or whatever the type of truth for direct logic is?

By negated application I mean depending on the negation of some other proposition. "The set of all sets that are not members of themselves" is only a paradox because of the negation. "The set of all sets that are members of themselves" is not a paradox. So you only allow ranks less than when it is negated. Allowing less than or equal in the non negated case is sufficient.

I'm not really sure if "inconsistency-robust" really means "paraconsistent" (or, at least, if the former is a special case of the latter), but, if this is the case, what you want outside of logic is the principle of explosion, not (necessarily) the law of the excluded middle.

Paraconsistency is a special case of Inconsistency Robustness. For example, intuitionistic logic is paraconsistent but not inconsistency robust.

How is intuitionistic logic paraconsistent? If I understand correctly, "paraconsistent" means "the entailment relation isn't explosive", i.e., there are inconsistencies from which not everything is derivable. Under this definition, intuitionistic logic isn't paraconsistent.

That being said, I'm very interested in your idea of inconsistency robustness, as a paradigm for developing and using distributed databases. I can't say I fully understand the exact meaning you associate to the term "inconsistency robustness", but it is clear to me that if there are multiple sets of evolving beliefs about the same domain of discourse, it will be the norm, not the exception, that some of these beliefs will contradict each other.

Could you tell me what papers I should begin reading?

Intutionistic logic is paraconsistent in that it is not the case that every proposition can be inferred from a contradiction.

For more information on Inconsistency Robustness, see Formalizing common sense reasoning

I think Hewitt is saying that in intuitionistic logic, a contradiction lets you derive every negated (and double-negated...) propositon, but not necessarily the non-negated ones.

Presentations I've read have an elimination rule for contradiction that allows you to conclude any other proposition. Wikipedia agrees. See the rule labeled FALSE.

Yeah, I think what Hewitt's talking about is minimal logic, not intuitionistic logic.

Proposition is not type Boolean (nor is it type Heyting); the Peano induction predicate is type Boolean^ℕ.

Thinking about this another way, is type checking decidable? If we assert proposition A has type B this can be true or false, but if it is not decidable then proposition A has type (B or not B) is not true. IE can type checking be inconsistent, and therefore we need to use an inconsistency robust logic to reason about it?

Type checking is rapidly decidable in ActorScript because it is very important for IDE responsiveness and error reporting.

(btw: I think I am using the DL vocabulary a little more properly if I say that propositions are boolean expressions, rather than "sentences", although a proposition is also a sentence.)

A proposition is an expression that, syntactically, is of Boolean type.

DL is able to prove itself inferentially incomplete, meaning that for some propositions, P, neither P or not P can be proved. Not every boolean expression can be reduced to a boolean value.

If the law of the excluded middle does not hold (IE neither P can be true) then they are not Boolean. Boolean algebra includes the law of the excluded middle and operates on bits (true/false) values. Saying something is Boolean implies it is a bit and it obeys all the axioms of Boolean algebra. To me the type sounds more like Heytingean, IE a bit that follows the axioms of Heyting algebra, which is the algebra used in proof theory and does not include the law of the excluded middle.

If they follow the axioms of Direct Logic, then they are neither Boolean or Heytingean. You would have to ask which algebra encodes the rules of Direct Logic. Boolean = classical logic, Heytingean = intuitional logic, what is Direct Logic?

I think I have not been precise enough in language.

Sentences are abstract grammar trees. These grammar trees are treated directly as mathematical objects.

Sentences with no free variables are propositions.

If a sentence can be reduced, it can be reduced to a boolean. This is guaranteed by the syntactic types of sentences and the rules of inference. This is the sense in which propositions are "expressions of boolean type."

Propositions are not expressions. In particular a Proposition is not Expression◅Boolean▻.

A sentence with no free variables can be abstracted to be a proposition.

Do propositions evaluate to expressions in DL?

Excluded Middle holds in Classical Direct Logic but not Inconsistency Robust Direct Logic.
Laws for Boolean algebra hold.
See Formalizing common sense reasoning

However, Proposition is not the same type as Boolean, nor it is the same type as Heyting.

How would I reason about code then. Lets say I have a sort function, and I want to write a proposition that is true if the code correctly sorts. This "truth" is obviously not Boolean because it might not be possible to prove the proposition, and Boolean algebra requires that (P or not P).

That's not the definition I gave, so debunking it doesn't invalidate mine.

That's not the definition [of Z] I gave, so debunking it doesn't invalidate mine.

Your definition, stripped of types for the moment, is this:

  Z.[f] -> [x] -> f.[Z.[f]].[x]

which is actually Y, not Z. In particular, it diverges in a strict language. I substituted a correct definition of Z.

In particular, it diverges in a strict language.

It does not:

// JavaScript code

function z(f) {
    return function (x) {
        return f(z(f))(x);
    };
}

z(function (factorial) {
    return function (n) {
        return n === 0 ?
            1 :
            n * factorial(n - 1);
    };
})(3)

// returns 6

You are right. I made a stupid mistake, misinterpreting your definition as a result. I will get back to you on the typing question.

According to your definition for Z:

1. Z can only fix functions whose type follows the schema ([[a]↦b]↦([a]↦b)).

2. Z is only guaranteed to be accurate for a subset of its range. It can not be accurate if the fixed point sought is not expressible as a total, computable function.

3. Even if the fixed point sought is expressible as a total computable function, the desired total computable function in question may not be derivable from the argument provided Z.

Regarding points 2 and 3: Procedures of type [a]↦b can be partial. See Hewitt's comment "Total math functions: different from executable procedures" elsewhere in this thread.

1. Z can only fix functions whose type follows the schema ([[a]↦b]↦([a]↦b)).

If you think [a]↦b is too much of a restriction on the type of a fixed point, I recommend setting a to be the unit type. Then it's comparable to what the Y combinator does in a lazy language; we're just tracking the laziness of b explicitly in the type.

(Well, "lazy" is an overloaded term. This simulated laziness is call-by-name rather than Haskell's call-by-need.)

2. Z is only guaranteed to be accurate for a subset of its range.

What do you mean by "accurate" here?

What do you mean by "accurate" here?

I think that, interpreted with strict semantics, Z.[f] can diverge rather than finding a fixed point.

Sketch:

f.[g:int |-> int] |-> int |-> int ===
  [x:int]:int ->
    let y = g.[x - 1]
      ((y == 1) && (x < 2)) ? 1 : x * y

ff.[x:int]:int -> (x < 0) ? 1 : !x

"ff" is factorial for integers >= 0, and 1 for integers less than 0.

"ff" is a fixed point of "f".

"Z.[f].[x]" diverges.

Nice, I was wondering how to construct an example like that one.

One function that has lots of fixed points but doesn't make them easy to calculate is the identity function. Your function's a better example because (I think) it uniquely determines a fixed point, but still doesn't give us the ability to compute it under an eager evaluation strategy. (In fact, I don't think it lets us compute Z.[f].[x] or Y.[f].[x] under a lazy strategy either.)

The reason I was hoping for an example like this was so that I could talk about how this imperfection probably doesn't matter to Keean Schupke and marco.

When they talk about how much they would prefer to use languages that let them define fixed point combinators, they seem to be okay with taking on the burden of responsibility to avoid nontermination in their programs. If they try to define factorial in the way you've shown and it diverges, they can consider it a buggy program and try again.

f :: (int -> int) -> (int -> int)
f g x = g (x-1) * 0
ff x = 0

.

Is it valid ActorScript though?

Edit: It looks like it is valid, and your argument is that this is not the 'Y' combinator?

Can someone confirm this?

Currently, there is no publicly available implementation of ActorScript.

In theory, that is true.

your argument is that this is not the 'Y' combinator?

Ross Angle defined Z this way:

Z◅a, b▻.[f:([[a]↦b]↦([a]↦b))]:([a]↦b) ≡
    [x:a]→ (f.[Z◅a, b▻.[f]]).[x]

According to that definition:

1. Z can only fix functions whose type follows the schema ([[a]↦b]↦([a]↦b)).

2. These typed versions of Z are only guaranteed to be accurate for a subset of their ranges. They can not be accurate if the fixed point sought is not expressible as a total computable function.

3. Even if the fixed point sought is expressible as a total computable function, the desired total computable function in question may not be derivable from the argument provided Z.

The following definition of RossAngleY in ActorScript is not the definition of the Y combinator:

Grr. I just spent an hour coming up with that translation only to find you'd just posted it.

Dear shap,

Thanks for your thoughtful comment.

I would greatly appreciate your pointing out any ambiguities that you find in my comments.

However, it is impossible to reiterate on LtU the entire contents of the articles on HAL from the book "Inconsistency Robustness".
Consequently, it is necessary to make references to the articles.

Also, the articles on HAL are at the leading edge of research (and consequently may have some bugs and ambiguities).
Of course, there are still some open issues currently being investigated.

Regards,
Carl

May I suggest you simply put some fibrations and adjoint functors in the mix? People will more easily recognize it as leading research in that manner. All the terms, typing, and logic is somewhat seventies to most people, I gather.

The problem isn't the vintage of the buzzwords. It's that when asked to connect the dots on his reasoning, he doesn't. More modern buzzwords aren't necessary with valid reasoning, and don't help without it. As time has gone on, circumstantial evidence has accumulated that his extraordinary claims are due to various gaps in reasoning that cannot be filled. Shap has captured it well, I think: the two likely alternative explanations for the bad impression he's created are that he gets it but can't express it, or that he doesn't get it. Whichever problem applies, unless he's able to recognize and fix the problem, he'd accomplish more by leaving off the mathematical foundations stuff and concentrating on other kinds of research.

Yeah well. My personal observation is that category theory and ActorScript stand on the same footing: both purely syntactic formalisms with little to none formal semantics. It isn't unprecedented, in the functional field you have Z, Bird-Meertens, and the somewhat unknown Funmath; purely syntactic works with little to none theoretical or tooling backing and often heralded by strong claims from fanatic proponents. Looks like these formalisms are dying off though.

This is just how the world used to work. So, I'll cut the guy some slack.

In the article, formal semantics of ActorScript is in the meta-constructs.

Hint: this is somewhat analogous to writing the Eval procedure for Lisp in Lisp.

Yah. I somewhat got lost when reading the type checking rules.

Type checking rules of ActorScript are very strict.

I would be happy to address any questions that you might have.

If anyone speaks in a tongue, it should be by two or at the most three, and each in turn, and one must interpret; but if there is no interpreter, he must keep silent in the church; and let him speak to himself and to God.

Unfortunately, category theory is not much help in software engineering :-(

Warning: high ferrous content in this message ;-)

I have complained on LtU somewhere before that I don't believe in the Haskell manner of exposing trivialities about functional models implemented, and trying to lift the exposed trivialities in order to reuse certain algorithms.

I've never been impressed that using high-powered category theory is useful in practice, no. I have observed that it can be quite illuminating — on a conceptual level, not a technical one — to ask, what are the morphisms, what are the categories, and even how do these things fit together into an adjunction. It can be quite fascinating to draw a "twisted hour-glass" and label the parts of it. (You can see what I mean by "twisted hour-glass" on page 8 of this pdf). But that's not the way category theory is being used in Haskell etc.; it's category theory as an aid to thinking, rather than as a technical device.

John,

Thanks for the link to your article Monads for Programming Languages.

Unfortunately, your article neglects to say that monads originate in the work of Scott, Strachey, and Milne:

* Dana Scott and Christopher Strachey. 
  "Toward a mathematical semantics for computer languages"
  Oxford Programming Research Group Technical Monograph. PRG-6. 1971
* Robert Milne and Christopher Strachey. 
  "A Theory of Programming Language Semantics"
  Chapman and Hall. 1976.

Your article also neglects to say that monads are unsuited for concurrency :-(

Regards,
Carl

PS. Based on reading your article, you should be careful about "The pot calling the kettle black" when it comes to the pedagogy of scientific artcles ;-)

I like your article and the manner in which it reflects on Wadler's work. I also liked your presentation of category theory.

To put it blunt: It's bloody nice to read a critique once in a while instead of mindless non-critical thinking exposed in too many papers these days. Groupies and fanboys, whatever happened to critical thought?

I disagree somewhat with your remark with that's how category theory is used in Haskell. Like people abuse C++'s template system to concoct the weirdest non-trivial solutions I gather there are some functional programmers who think that they should expose the most trivial structures and make sure they use the monad, functor, or whatever type class to structure their program instead of simply stating a functional program directly.

I see little use for category theory in software engineering. An arrow has a beginning and an end, and you can compose them - that's the heart of category theory and that's simply too trivial an observation to be of much help to the hard problems often encountered.

From my dissertation:

Confusion may be avoided later by recognizing, at the outset, that there are no universally agreed-upon boundaries for logic and mathematics. Rather, each of the two subjects is pursued by a living community, and so ultimately each is defined by its community: logic is what logicians study, and mathematics is what mathematicians study. Historically, logic is the study of inference, and mathematics is the study of number; and this might still be claimed, since study of inference can be stretched to include nearly any reasoning, while number can be stretched to include nearly anything reasoned about; but in practice, rapid technological expansion of mathematics over the past four and a half centuries, and of logic over the past one and a half, has provided great scope for disagreement over the boundaries of both disciplines.

Those are assertions you make and Hewitt is making a contra assertion in the domain of "mathematics". The conflict here is (suddenly) pretty sensible to me and interesting.

To review:

ca. 1920 the foundational question arises: is there a finite set of axioms or axiom schema that spans all of math?

ca. Turing, Goedel, Church: every finite set of axioms or axiom schema is either incomplete or inconsistent

ca. Hewitt: Formal mathematics is an activity that can be formally described by a syntax for propositions, alongside some simple mechanical rules for transforming given sets of propositions into concluded sets of propositions based on very conservatively chosen rules of inference.

Within such a formalization of all of math, familiar mathematical concepts like "theory" appear as syntactic types.

This kind of formal system contains every theorem in every branch of mathematics. Every theorem appears as A-turnstile-B where A states the axioms of some theory and B, a theorem in that theory. (If A is empty, if a proposition B follows just from the formal rules of mathematics, it's just "turnstile B").

Mathematics, as Hewitt has formalized, is able to convincingly demonstrate by model that it contains no sentence which contains a self-encoding.

Mathematics, as Hewitt has formalized, is able to convincingly demonstrate by model that it is complete in the sense that all constructible propositions following from a given set of propositions can be computed.

And as formalized the system proves its own self-consistency.

----------------------

Shutt (the quote you posted) and Hewitt part ways over whether it is possible that Hewitt has, in every reasonable sense of the term, circumscribed all mathematical discourse possible. That is, anything that can't be expressed in his formalization, probably people will generally agree isn't mathematics. Whether they know of Hewitt's results or not -- it would turn out they would agree. I think underneath it all, he's basically got a simple and powerful system.

Does he have a pretty cleanly constructed system that, really, is pretty much all the "foundation of math" we'll ever get from anyone?

I also think he's thinking about what happens if you model the formalization of math as actors, in various ways, so that sets of propositions are just things wandering around through actor-space, getting soundly transformed and passed along at every node.

Some miscellaneous comments:

The point of the pasage I quoted was to warn against getting mired in (and oneself not to get mired in) philosophical discussions of what mathematics is when all such philosophical discussions are illusory. So you'll understand why I'm not inclined to discuss philosophically what is mathematics.

Notwithstanding whatever casual shorthand anyone (including me) might use for it, the foundational issue that gained public visibility circa 1900 was not axioms encompassing all of mathematics, but axioms encompassing arithmetic.

Hewitt is quite explicitly exclusionary; he makes much of this. Moreover, in order to avoid Gödel's Theorems he doesn't just have to avoid making an explicitly self-referential statement, he has to avoid being able to reason in pretty elementary ways about arithmetic functions. There's no way that isn't exclusionary, even if he weren't bible-thumping about the need to exclude things.

This, in turn, leaves three possibilities: either he has a system that doesn't really avoid Gödel, or he has a system that avoids Gödel by not meeting Gödel's "sufficiently powerful" condition, or he doesn't have a well-enough defined system to be able to meaningfully judge whether or not it avoids Gödel.

Notwithstanding whatever casual shorthand anyone (including me) might use for it, the foundational issue that gained public visibility circa 1900 was not axioms encompassing all of mathematics, but axioms encompassing arithmetic.

Thanks. I corrected it to say "ca. 1920".

Moreover, in order to avoid Gödel's Theorems he doesn't just have to avoid making an explicitly self-referential statement, he has to avoid being able to reason in pretty elementary ways about arithmetic functions.

You can define the logic you want for arithmetic functions in a theory T and make proofs of the form "T |- P".

This, in turn, leaves three possibilities: either he has a system that doesn't really avoid Gödel, or he has a system that avoids Gödel by not meeting Gödel's "sufficiently powerful" condition, or he doesn't have a well-enough defined system to be able to meaningfully judge whether or not it avoids Gödel.

It's the fourth one in your list. :-)

If you want extra axioms, A, for arithmetic, your proofs will have the form "A |- P". If your axioms are provably buggy, you can prove something like "|- (A |- B) and (A |- not(B))". You'll have something like "|- Inconsistent (A)". But the system (Hewitt's) in which you're doing all this... hasn't been rendered inconsistent at any step here.

This is just a formalization of the observation that people can tell if formalized math is rigorous using pretty weak, robust logic. Math in general is a formalizable as a system for making those judgements. Math in general contains terms that are theories about richer proposed sets of axioms.

A big part of the point of Gödel's results, of why they're a big deal, is that you can't avoid them through indirection.

Gödel's results depend on a funny kind of indirection depending on a nonexistent fixed point

Goedel's second theorem produces a proof schema which can't be applied if sentences can not be internally defined by fixpoint operation.

Goedel's "incompleteness" says basically that a finite set of hypotheses doesn't yield all arithmetic truths as direct implications. In fact, the first theorem tells you how to take any finite set of arithmetic hypotheses (that is consistent) and generate a new, compatible hypothesis that can't be proved from the originals.

Hewitt's system contains all propositions Goedel can generate that way and makes them available as hypotheses (to sit on the left side of a turnstile).

I think you're giving too much credit to what Hewitt's system accomplishes. As far as I can tell, you can replace the turnstile with an arrow (moving the subscript to the left or adding 'true' to the left if there is no subscript) without changing the semantics any. So how is this different from just using second order logic as a foundation for mathematics?

If you take second order logic without any other axioms, that's consistent and complete! You can already use second order logic as a foundation of mathematics in the way you're describing. Just put the theory you're interested in as a hypothesis (LHS of an implication). But that's not interesting.

Godel's first theorem establishes a limitation on what you can prove to be true about arithmetic. Whatever formal system Hewitt has in mind, it won't be able to prove all and only true propositions about the natural numbers, because there's no way around that aspect of Godel. Honestly, I'd find Hewitt's spiel less annoying if he would least acknowledge his understanding of what Godel did actually prove and how it applies to his system instead of implying that Godel just made an error somewhere.

To turn second order logic into a theory of math-in-general wouldn't it have to be augmented with definitions for domains like sentences and proofs and theories and in that capacity also have enough to serve as its own metatheory?

Doing that naively would risk creating a too strong system in which a Goedel theorem 2 style argument could be made?

If you can model sentences and proofs and theories by erasing those things, then they aren't going to be the cause of inconsistency. And again, as far as I can tell, you can model sentences, proofs and theories with ordinary propositions. That is, there seems to be a scheme of rewriting one of Hewitt's propositions that makes use of turnstiles and proofs and sentences and quoting/dequoting into one that doesn't by just projection down onto ordinary propositions and implication.

This allows for a soundness proof, through the observation that these features could be literally meaningless. Now if you added the ability to treat proofs, sentences, etc. as data that can be inspected, combined, quantified over, etc. then that would make it so that you can't just erase these elements. But then you'd be inconsistent.

If you can model sentences and proofs and theories by erasing those things, then they aren't going to be the cause of inconsistency

If you want to model them in 2nd order logic you'll have to give construction rules for members of the classes. If you want to model them with fidelity, your rules will include the type restrictions that characterizes them in Hewitt's system.

In short, if it works you'll have just written a bunch of new definitions that are isomorphic to Hewitt's. You won't have "erased" anything.

The erasing happens when you go to give meaning to those definitions. We can work in a system that already has a type system. In that case you just erase the part of the type that claims to be doing the encoding. Quoted T just becomes T. Sentence T just becomes T. You shouldn't just look at the symbols he uses to decide what they mean. You should look at what you're allowed to do with the symbols to decide what they mean. His turnstile doesn't capture probability if you can't inspect proofs as data.

The erasing happens when you go to give meaning to those definitions.

That and the sentences follow it in your comment have no obvious meaning.

Earlier you seemed to propose that Hewitt's foundation could be modeled by some other proposed foundation which, well, one would hope. And you seemed to suggest that implied odd things about how much credit anyone deserved, something like that.

Beyond that I'm not so sure what your point is.

Hewitt claims that mathematics proves its own consistency. His proof is that ⊢Ψ implies Ψ and ⊢¬Ψ implies ¬Ψ, and so we have a contradiction (Ψ and ¬Ψ). But why should I interpret the form "⊢Ψ" as asserting the provability of Ψ? He could have just as easily used ☺ Ψ instead of ⊢Ψ. So why interpret the turnstile as asserting provability?

We can observe that DirectLogic is consistent (AFAICT) by interpreting "⊢Ψ" as meaning "it is true that Ψ" rather than "it is provable that Ψ". This interpretation of turnstile makes it a no-op (erasable). There is no difference in this particular model between Ψ and ⊢Ψ. With this interpretation, the proof of the consistency of mathematics can be read as simply asserting that if mathematics contains a contradiction, then it contains a contradiction.

But I suspect the situation is actually worse than that. Hewitt would like you to read "⊢Ψ" as asserting the provability of Ψ. By the above argument (informal by necessity since a formal definition of DirectLogic doesn't exist), we don't have to interpret that way. But we can ask, is it possible to interpret the turnstile the way Hewitt intends? Is there a model of DirectLogic in which the turnstile is interpreted as asserting the existence of a proof of Ψ? I think the answer is "no". If you did have such a model, then you'd be able to consistently expose the kind of reasoning that would get you in trouble with Gödel's second theorem.

Regarding my statement that you're giving Hewitt too much credit, that was a poor phrasing. In this specific instance, I think you're overestimating the importance of what DirectLogic accomplishes because of the above. I find Hewitt's writing more sensible than I used to as I've been able to understand his language a little more. I still think his characterization of the Gödel incompleteness theorems is off the mark, but I have no interest in denying him whatever credit he's due.

Provability (⊢) is different from truth (⊧).

In particular, true in the model ℕ is different from provability in the Peano/Dedekind categorical axiomatization for ℕ.

See page 15 of Inconsistency Robustness in Foundations.

PS. When it comes credit, colleagues and students did a lot of the work!

Again, it looks like I can interpret "⊧Ψ" as "Ψ is true", so all of this is probably consistent, but you (AFAICT) haven't demonstrated that a model of DirectLogic exists in which the symbols all mean what you intend for them to mean. And I'm skeptical that such a model exists.

Because Direct Logic is much more powerful than Tarskian set semantics, it has no Tarskian set semantics.

However, Direct Logic does formalize the Tarskian set semantics for the Peano/Dedekind categorical axiomatization of ℕ and prove the inferential incompleteness theorem for ℕ.

A consequence is that there are true but unprovable propositions in ℕ.

Because Direct Logic is much more powerful than Tarskian set semantics, it has no Tarskian set semantics.

Do you have anything to offer in the way of proof of that claim (which I find dubious)?

Tarskian set semantics has no way to deal with propositions involving inference (⊢), e.g classical soundness:

ForAll[p:Proposition]-> (⊢p) => p

DirectLogic must be stronger than set theory because your intended interpretation of DirectLogic isn't sound in set theory. That's a good one :).

Classic inference (⊢p) is intended to mean that there exists a proof of p. A proof is a finite object and so of course set theory has no trouble encoding that relation. What is your interpretation of ⊢?

Doing a Tarskian set semantics for inference (⊢) is difficult.

You can be first ;-)

:)

A proof is a finite object and so of course set theory has no trouble encoding that relation.

Sentences are abstract objects in DL. Some but not all Sentences can be obtained by parsing finite strings.

Sentences have the general form of a syntax tree of the sort you would expect except that...

Actors (which is to say arbitrary, non-deterministic, unbounded-in-general computations) can be used as terminals in sentences. The example in the paper is Sentences over real numbers considered as Actors that lazily produce successive digits of precision.

If ⊢p doesn't assert the existence of a finite proof object proving p, then I don't know what it means and will wait for someone to tell me.

If ⊢p doesn't assert the existence of a finite proof object proving p, then I don't know what it means and will wait for someone to tell me.

Presumably Actors as terms in sentences tells us that proofs are validated by evaluation, but evaluation is not guaranteed to terminate.

For example, a nondeterministic Actor can produce a random real number in [0,1] as mentioned in the paper.

An attempted proof that two of those numbers have the first K digits for finite K would terminate. An attempted proof that they are equal might or might not terminate.

If I want to read the statement of a theorem about "those two numbers," the random reals output by a non-deterministic Actor, do I need to wait for them to finish outputting an infinite number of digits, so that I can read them all? Or am I reading a statement which contains a description of that Actor computation, and then interpreting the statement to be about their potential output? I'm not sure why we'd want to humor infinite-length theorem statements, if it's the first case (call me a stickler, but if you say you have proved something, I'll probably demand to at least be able to read the claim in finite time; if I'm feeling particularly stubborn, I might also demand to see a proof that I can read in finite time too). If it's the second case, then we obviously have a countable set of sentences, at the meta-level.

Seriously, though, I get why internal to the system you'd want sentences to be uncountable, the way things are set up. I just don't get why we're not permitted to reason at the meta level (by, for example, making the observation that, externally, sentences are countable).

Regarding these proofs, if they are Actor computations, presumably they have finite descriptions. Why can't these descriptions themselves (instead of their evaluation) be the proof objects?

I'm not sure why we'd want to humor infinite-length theorem statements,

Indeed. Here are some suggestions of why we might choose to:

DL seeks to be a foundation for mathematics but in particular a foundation for mathematics for computer science.

DL uses a nicely general model of computation that includes unbounded, non-deterministic computation. A hardware device that uses some suitable quantum signal to generate (over time) a never-ending sequence of 0 and 1 bits is an example. Such a hardware device could be a particularly nice implementation of the real-number-generator example in the paper (defined by a program text that non-deterministically chooses 0 or 1 as the next digit, and then postpones similar generation of further digits until they are needed).

Parsimony suggests we go ahead and do what is possible: Unify such computations with various sets and classes that, heretofore, mathematicians have often treated simply as given constants.

In orthodox math we have a weird situation where some domains, such as reals, can not have every member denoted by some finite string ..... and so mathematical utterances written on paper as strings are confined to talk only about sub-domains of "constructable" reals or to talk about classes of abstract reals.

The real world, for all practical purposes, contains actual reals which neither constructable in that old sense nor are they a class -- they are a specific real. The device that measure electron spin and spews out random 0s and 1s endlessly is an example (or can be interpreted as such).

Reifying that output, our example infinite real from the hardware device, in a programming language, we get a value that is in every way isomorphic to some real in [0, 1]. We so happen to be able to effectively access its digits one after another, over time.

Presumptively the real number corresponding to our reified random bit generator is not a constructable real. Nevertheless, whatever our program does with this reified value amounts to proving theorems about it.

Well, shouldn't a foundation of mathematics, especially a foundation of mathematics for computer science, recognize that kind of proof?

Surely there are other approaches to "dealing with" the kinds of "infinite" values the hardware device gives us but that isn't the point. It isn't the point that DL is a unique way to reason about these kinds of things. It merely aims to be a comprehensive, parsimonious, useful way.

I suggest you and Hewitt converse privately about it. Maybe you can get a peer-reviewed article accepted.

I'm discussing one of the papers. What are you doing?

I suggest you and Hewitt converse privately about it. Maybe you can get a peer-reviewed article accepted.

He has an informal system which he makes wild claims about, and a programming language which barely exists on paper.

If you feel discussing it, be my guest. Guess I got tired of reading all the bullshit about things which don't exist.

Of course, you can discuss things which don't exist ad infinitum, be my guest.

I am out.

I don't have any strong feelings against DL itself, and sure, it can probably function well as a foundation of mathematics. (Mathematics is robust enough that the particular choice of foundations doesn't matter so much: high level arguments will look the same, but there may be some low-level details that change).

I also wanted to draw attention to constructive accounts of the reals which admit both the orthodox classical reals as a model, and a countable model of computable reals. In such settings we can freely talk about "reals" without committing to either model: everything we deduce applies equally to the classical reals and to the constructable reals. (I know you specified orthodox, and these accounts aren't exactly mainstream.)

Regarding your hardware example, I don't really get it, as at any time, the program has only seen a finite prefix of the "infinite" bit string generated by the device, so I would think it can only have "proven" things about these finite bit strings. If we're talking real life, then obviously there is no sense in which the device can generate an infinite bit string. What do we gain by pretending it can? Especially over an equally unrealistic assumption, that it can generate a finite bit string of any length? Even if you want to model things by pretending they can run forever, I'm still not seeing why we would want to allow infinite proofs.

I don't really get it, as at any time, the program has only seen a finite prefix of the "infinite" bit string generated by the device, so I would think it can only have "proven" things about these finite bit strings.

The rationale I am offering is one of parsimony. As an example, suppose that I have two actors supplying a real in [0,1] as a lazy stream of bits. I can inductively define their sums and products. I can establish various algebraic relations among them. My program can reason with these arithmetic relations even if there is no upper bound on how long it might take to produce the first bit of a sum.

I'm still not seeing why we would want to allow infinite proofs.

Since these have practical implementations such proofs are in a useful sense about the real world.

I can follow modeling arithmetic on reals that way, I've got no problem with that. You can do it in other ways (I've actually worked on things pretty close to this), but as you say, that's not the point.

Where you lose me, is with the infinite proofs. I'm guessing, if I asked you to show me, in this hypothetical scenario, just how you established the various algebraic relations among the arithmetic operations, you'd be showing me some finite set of symbols on the screen. Perhaps code. Perhaps a logical proof. I think I'd be pretty confused if you told me to wait while you ran an infinite non deterministic Actor computation. In other words, even if you're proving things about infinite computations, I'd still expect finite proofs.

DL is meant to be a "foundation for mathematics for computer science"

As a "foundation for mathematics" it is meant to be:

1. A foundation that can be built on to make other more specialized mathematical theories.

2. A meta-theory for mathematical theories in general.

Since DL is meant to be the "root" theory, the meta-theory of theories, it serves as its own meta-theory.

As its own meta-theory, it can reason in a first-class way about its own Strings, Sentences, Propositions, Proofs, and so forth.

It's a reflective theory, in that way.

The DL paper linked above specifically calls the notion of a sentence that could be described as:

"3.1415.... = 3.1415...."

That's an informal string and it is meant that you imagine the elipses replaced with all the digits of pi.

You can't build that as a string and then parse it.

But you can abstractly build a syntax tree (a Sentence) with those terms. And you can concretely build a value in a computing system that usefully reifies that sentence for all practical purposes.

As a human activity you have proofs going on in both areas: proofs about abstract sentences that can include arbitrary reals as terms. Proofs about concrete sentences that can include things like reified reals whose digits are computed as needed for whatever kind of inference your making (or whatever).

All those different activities have a common logical structure. DL (at least tries) to give you a parsimonious way to talk about that over-arching mathematical logic.

I think I'd be pretty confused if you told me to wait while you ran an infinite non deterministic Actor computation.

In a common case, your browser would just time out. :-)

I'm accustomed to systems where proofs are programs, but we don't have to run them, but merely type-check them. Some of these programs are co-fixpoints, so they run "forever". So this is part of the disconnect for me. I would have thought, it ought to suffice to read the "source code" that's generating whatever is counting as proof objects. But I'll have to think about it more. I've also noticed something like staging seems to be at play here, and I think I'd better give that more careful thought, as well.

I have no problem envisioning that sentence "pi = pi" as an abstract sentence. In the version in my head, the nodes of type real at the bottom hold the concrete instance given by a procedure that computes pi to arbitrary precision. The whole thing has a finite description. Internally, yes, there are uncountably many sentences equating two reals. But I fail to see why we can't observe that externally, there are countably many such sentences. If we're talking practical, then I'd think this is all going to end up in a computer implementation, with DL "source code". It's hard to get away from the countability of code. Maybe one way to say this is that DL admits a countable model, even though it doesn't think it does (Skolem's paradox).

Re: "It's hard to get away from the countability of code."

Actors are not the code that (non-deterministically) defines their behavior. Informally, intuitively, think of an Actor as a running instance of the code, not the code itself. Since actors can be non-deterministic, the code alone doesn't identify a particular Actor.

(Note that I reregisterred on this site just to make this comment and I am very much otherwise out of my depth here.)

You might be interested in the arguments and work developed by Professor Norman Wildberger as express via his YouTube channel.

One popular but controversial video/lecture that seems to me to be somewhat relevant here is
MF80: Inconvenient truths about sqrt(2) which is part on his Math Foundations series/playlist in which he builds up the number mathematics part of the broader "mathematics" as has been discussed here.

You may enjoy his methodical, step-by-step, no hand waving developement that enables exact proofs and calculations by avoiding infinite "numbers" and infinite processes.

Can someone please fix that?

Regarding these proofs, if they are Actor computations, presumably they have finite descriptions. Why can't these descriptions themselves (instead of their evaluation) be the proof objects?

Non-determinism means that an Actor programs don't necessarily specify a specific value.

I'm having a hard time connecting this to anything familiar. In evaluating these non-deterministic actors, is it possible we get failure, i.e., a non-proof? Is non-termination admissible as a proof? There are plenty of proofs in orthodox mathematics that describe procedures that make arbitrary choices, but of course the point is that the choices don't matter. I was guessing something like this could be going on when I suggested the description should suffice. If the evaluation might fail, with a non-proof, then it seems like we need to do the evaluation first, before we can claim to have a proof (perhaps in the form of a finite execution trace?)

If the evaluation might fail, with a non-proof, then it seems like we need to do the evaluation first, before we can claim to have a proof (perhaps in the form of a finite execution trace?)

Right. If your program is trying to check a proof and the proof has been constructed with some term that refies some Actor, then there is a possibility that the failure of that Actor to return a value will in turn "hang" the proof check.

That doesn't mean that the structure of the proof is mathematically invalid or that your method for checking it is invalid. It only means the correctness of the proof might be undecidable.

I think this gets to the bottom of things, as I definitely take decidability of correctness as part of what being a "proof" means. I thought the whole point of a proof was to convince, and not being able to check a proof would seem to defeat that. But I'll just make sure I translate "proof" to something else (I'm going to call it "semi-proof" to myself, for now, like semidecidable), when I read about DL in the future. This may read as being sarcastic, but I don't mean to be. It's rather tricky to absorb all of the new definitions for terms that's required to make sense of Hewitt's system.

[...] it has no Tarskian set semantics.

Do you have anything to offer in the way of proof of that claim (which I find dubious)?

Please forgive me if all I do here is expose some misunderstanding on my part but...

DL can apparently prove that some of its propositions are undecideable and infer that such propositions and their negations are both true, albeit unprovable.

Doesn't that imply that no model exists?

DL can apparently prove that some of its propositions are undecideable and infer that such propositions and their negations are both true

That would seem to immediately imply that DL is inconsistent, so I think you've remembered or stated that wrong. Can you find a link to that?

Doesn't that imply that no model exists?

It's my guess that a set theoretic model of DL does exist -- namely, the erasure-semantics model that just interprets ⊢p the same way it interprets p.

In Direct Logic, ⊢Ψ does not mean the same thing as Ψ

Which axiom of DirectLogic lets us tell the difference?

Truth is not the same as provability because by the Church/Turing incompleteness theorem, there is a Ψ such that ⊧_ℕΨ but not ⊢_ℕΨ

I found your definition of 'closed theory'. How do you prove that ℕ is a closed theory? What does ⊢ mean in DirectLogic in the case that the theory is not closed?

I've spent too much time on this and until there is a formal account of DirectLogic, probably shouldn't spend any more time on it, but I wanted to refine my guess as to why DL is consistent.

At the top level, you're trying to encode mathematics as its experienced by mathematicians by defining ⊢ to mean "proven by unspecified mathematical argument" and not assuming the proofs of mathematics to be computationally enumerable (and, in fact, you can prove that they aren't). But note that, whatever axioms you choose, the theorems of DirectLogic will be computationally enumerable, even if you don't internalize this fact.

I think you can create a set theoretic model of DirectLogic by taking the provable sentences of mathematics (top level ⊢, in DirectLogic) to be all sentences that are actually true in the model. But for a particular enumerable theory X, there can still be a distinction between ⊧_X and ⊢_X in the model.

I don't see how you're ever going to get a handle on differentiating theorems that are provable by some nebulous mathematical argument (with no reference to a set of axioms) and theorems that are true but not provable by any nebulous mathematical argument.

Looks like Hewitt simply wants you to think over his thought experiment until you bite and do his homework.

I would advise against thinking about it too much.

The DL paper linked at the top answers a lot of your issues. For example, it more precisely explains what turnstile means and why. It explains pretty directly (constructively) why proofs aren't enumerable. It contains a formal syntax, core definitions, and axioms.

It is an overview and an exposition of motivations and responses to those motivations but it does have a lot of the harder stuff you complain is missing. I find it much better than some of the earlier condensations of more or less the same material. Not sure how much of that is because the text improved and how much because I got the gist after which the details start to come in focus.

Between asking "what does turnstile mean?" and the above post titled "erase at the top level", I (re-) read opening to the paper that introduces turnstile and figured out that there is supposed to be a distinction between DirectLogic and "mathematics". DirectLogic will have some computationally enumerable set of theorems that are provable in mathematics, but his ⊢ is intended to mean provable in some general system of mathematics (that presumably contains DirectLogic as a subset).

So the reason that Godel's second theorem won't apply internally to DirectLogic's ⊢ is its proofs aren't enumerable.

I still don't know how we know that e.g. ℕ is computationally enumerable, but I don't think it's that important. It's probably because we define ℕ in terms of the Peano axioms.

By the above reasoning that Mathematics contains DirectLogic, it seems true that for any statement Ψ that DirectLogic proves, we should have that ⊢ Ψ is true. This suggests to me that erasure (interpreting ⊢Ψ as Ψ in the model) should work as a semantics, which should probably lead to a set theoretic consistency proof. It also shows that we don't have to interpret ⊢ the way Hewitt intends.

Do you think I'm still missing something?

I do, based on what you just said. I'll try to be helpful. Conversely, please understand that I'm a naif in foundation debates. E.g., not all but quite a lot of the talk about relating to model theory is very hard for me to figure out.

You say:

I (re-) read opening to the paper that introduces turnstile and figured out that there is supposed to be a distinction between DirectLogic and "mathematics".

Rhetorically, the paper distinguishes between "mathematics" and "Mathematics".

The noun "mathematics" describes mainly the formalizable traces of the work of living labor... the activity of mathematicians present and historic. The historic social process of "mathematics" is retrospectively interpreted as one in which a proliferation of theories are each advanced. Some are internally inconsistent. Some are provably not. Some we can't tell, and so on. The society of mathematicians is robust in the sense that inconsistent theories which arise don't generate inconsistencies in any other theories (but their extensions). And there is a kind of very conservative, safe, overarching logic that unites the society of mathematicians in an evolving discussion about theories in general and the relations among particular theories.

A "foundation for mathematics" in the paper is conceived to be on the one hand a candidate logic to formalize that overarching conversation about theories in general, and on the other hand as a foundation that can be extended to create that proliferation of theories.

Classical Direct Logic is a proposed logic to serve as that foundation. It is arrogantly nicknamed "Mathematics".

DL is meant to be that foundational theory but it is in particular meant to be a "foundational theory of mathematics for computer science".

This gives rise to some of the unusual features of DL because the design of DL contemplates mathematical activities (e.g., generating and checking proofs) conducted autonomously by machine. As one example, close to the core of the thinking, DL maintains an explicit distinction between a string of symbols you might write on paper, and a sentence which is an abstract syntax tree. The distinction runs deep in the sense that DL allows the terms of sentences to include arbitary elements from uncountable sets as terms. Thus, not every Sentence in DL can be unparsed to produce a String.

DirectLogic will have some computationally enumerable set of theorems that are provable in mathematics,

You can define enumerable subsets of DL theorems but DL contains an uncountable number of theorems, I believe, since given any proposed enumeration it would not be hard to add new theorems by diagonalization.

⊢ is intended to mean provable in some general system of mathematics

It is meant to mean: provable using the syntax, domain definitions, and inference rules in the appendix.

So the reason that Godel's second theorem won't apply internally to DirectLogic's ⊢ is its proofs aren't enumerable.

No, Goedel's 2nd doesn't kill DL, in spite of DL's proof of self-consistency, because an inferentially self-referencing sentence can not be constructed. You can't construct a proposition PHI such that a proof of PHI formally implies, within DL itself, that PHI can not be proved.

By the above reasoning that Mathematics contains DirectLogic,

"Is" not "contains". Capital-M "Mathematics" is a nickname for "Classical Direct Logic". (I don't think the terminology is used with Bourbaki-style tight-buttedness throughout the exposition but you can see the idea there at least.)

it seems true that for any statement Ψ that DirectLogic proves, we should have that ⊢ Ψ is true.

By the definition of "⊢".

This suggests to me that erasure (interpreting ⊢Ψ as Ψ in the model) should work as a semantics,

I'm on ice thinner in this next answer than most, I think, but I'll try:

DL contains as first class objects other theories using (I think) the same syntax and definitions, with extensions allowed, and with alterations to inference rules allowed. I'm fuzzy on this but in any event you can create "sub-theories" for which DL is a meta-language and the sub-theories are first class objects in DL.

First, though I know this does not answer your question, the naked turnstile is useful notation just for keeping clear what is proved in what when using DL in meta-theory mode.

Second, still not quite answering you but getting closer: DL is meant to be useful as its own meta-theory, with its own proofs as first-class objects. "⊢Ψ" gives an abstract notation that says PSI has a proof.

Third, now I think I can make better sense of the answer Hewitt gave you to this question, the truth of PSI in DL is different from the existence of a proof of PSI in DL.

An undecidable PSI may be regarded as true and so too its negation. DL can't treat PSI as true or false in that case but it can hypothesize (for the sake of some argument) the truth of PSI without having to assume that the truth of PSI <=> PSI has a proof.

Does that help?

I appreciate the detailed attempt at clarifying what you think is going on. I found this quote in the opening paragraph:

Classical Direct Logic is a foundation of mathematics for Computer Science, which has a foundational theory (for convenience called “Mathematics”) that can be used in any other theory.

The way I read that, it seems that Classical Direct Logic is supposed to be a superset of Mathematics. I suppose Hewitt could provide clarification if he desired.

I have a hard time with this uncountable sentences bit for reasons similar to those named by James Lottes (at least I think for the same reasons - I skimmed that exchange).

I don't see how a proof could ever be something that wasn't checked in finite time. I can understand how sentences could be uncountable, but for those sentences to be proven true, it seems to me that only finitely much of the sentence could be involved in the proof. And thus you could always generate a finite sentence that represented what was proven. e.g. 3.1415926... > 3. I don't need to know what digits the ellipsis represent to prove this sentence.

Stated in more glib way, I have a windows machine and a linux machine here, but neither is a counterexample to Church's thesis, as far I know. So when Hewitt ships DirectLogic.exe to me and I start using it to prove theorems, the ones I'm able to prove will live in a computationally enumerable set.

But it would be problematic for the meaning of ⊢ in the logic to be the set of theorems provable by a computationally enumerable process, because the logic is capable of proving that there is no such enumeration. So it wouldn't be sound.

Anyway, I do appreciate the effort in communication, but I really need to stop thinking about this. I'll continue to read any posts you make on the subject, so if you figure something out and explain it, I'll read it. But I'm not going to spend any more time wading through the article.

Thanks for looking at the article.

Certainly, each proof has a finite number of steps :-)

I don't see how a proof could ever be something that wasn't checked in finite time. I can understand how sentences could be uncountable, but for those sentences to be proven true, it seems to me that only finitely much of the sentence could be involved in the proof. And thus you could always generate a finite sentence that represented what was proven. e.g. 3.1415926... > 3. I don't need to know what digits the ellipsis represent to prove this sentence.

DL says nothing at all about how long it takes to check a finite number of proof steps.

How long it takes could depend on what oracles your proof checker includes.

An example "oracle" would be an equality check for infinite streams of digits that can sometimes skip over infinitely many steps by using a (lisp-style) EQ? shortcut as a kind of implementation-specific internal hack.

How long a proof takes to check, in DL, has in the general case an undecidable lower bound.

My interpretation is that the turnstile is deliberately left open to that kind of Oracle or to axioms that weren't originally included in the schema. The way I was suggesting you could prove this sound is to assume the ultimate Oracle: the truth oracle that answers whether a proposition is true. This is another way of looking at erasure semantics -- view the naked turnstile as a truth Oracle.

What do you of this? On printed page 13 (pdf page 14) there's a proof by contradiction that "Mathematics is Open". The proof assumes a "provably computable total procedure Proof" such that it is provable that:

├^p Ψ ⇔ ∃ [i:N]→ Proof[i]=p

I believe that says PSI is provable by proof p if and only if there is some i such that p, a proof, is the value computed by Proof[i].

The argument continues by performing a diagonalization: "As a consequence of the above, there is a provably total procedure
ProvableComputableTotal that enumerates the provably total
computable procedures that can be used in the implementation of the
following procedure: ...". OK, so there is no such "Proof" procedure.

I'm not sure how we could erase the turnstile here.

The truth of PSI is clearly different in this theory from whether or not it is provable by a computable total total procedure.

To be reflective, to serve as its own meta-theory, DL needs a built-in alternative to Provability Logic (see printed page 38, PDF 39).

So to sum up this and the bit about equality-test oracles:

1. Whether or not a proposition is provable is not, in the general case, fully determined by the semantics of DL itself. It depends on the implementation. (And note that the proposition we are trying to prove may only ever exist within one implementation.)

2. In order for DL to make reflective arguments, such as about its own inferential incompleteness, the Mathematics (empty to the left, no theory subscript) turnstile can't be erased. That's because a proposition can clearly be true but unprovable, as illustrated by the ambiguity of provability in (1).

We're talking about a different piece of syntax, now:

├^p Ψ

What would a proof of Ψ look like for the truth oracle? It could just look like this:

Ψ. QED.

The catch is that this proof is only accepted by the oracle when Ψ is actually true. Thus proposition you quoted is just asserting, under this interpretation, that there is no computable enumeration of the true propositions.

But you might be right that you can't fully erase ├ Ψ down to true/false. If his logic allows you to reason that ├ Ψ iff there exists a proof p such that ├p Ψ, then we can't represent Ψ as true/false -- we need to remember the actual proposition (otherwise 'True. QED' would be a proof of any true proposition). I still think you can give it a simple semantics this way, though, where ├ Ψ means that Ψ is a true proposition.

I basically agree with your 1). The meaning of ├ is underspecified by DirectLogic in the sense that the axioms and inference rules of DirectLogic don't uniquely determine what it might be in a model of DirectLogic (probably, from what we've seen) . But I don't agree with your 2) because I think one particular model of DirectLogic could have the naked turnstile meaning "it is true that".

It is impossible to computationally enumerate the true propositions of the Peano/Dedekind categorical axiomatization of ℕ.

Church's paradox is that the theorems of Mathematics are not computationally enumerable. See page 40 of Inconsistency Robustness in Foundations.

[Franzén 2004] argued that mathematics is inexhaustible because of inferential undecidability of mathematical theories. The theorem that mathematics is open provides another independent argument for the inexhaustibility of mathematics.

Direct Logic can:
* define Tarskian set theory semantic satisfiabilty for the Peano/Dedekind categorical axiomatization of the theory ℕ
* use the above semantics to prove that there are true but unprovable propositions in the theory ℕ.

However, there is no Tarskian set theory semantics for Mathematics.

true but unprovable propositions

Is it possible in DL to make a construction like this:

An actor of sort Rand01 is like the one in that paper that returns a non-deterministic, infinite list of binary digits.

An actor of sort Zeros returns an infinite list of 0s.

An Actor of sort ZerosOrRand01 returns an infinite list of binary digits. Based on a non-deterministic choice before the first digit is returned, it decides to act either as a Zeros Actor or a Rand01 Actor.

Can there be a class of propositions in which the equality of pairs of Actors of sort ZerosOrRand01 is asserted?

Is there then not a further final proposition that asserts all members of that class are decidable?

Is that final proposition not provably undecidable?

Church/Turing first proved that all true propositon of N cannot be proved. (Godel's proof is invalid because he used a "self-referential" proposition based on a non-existent fixed point.)

Please see page 14-15 of Inconsistency Robustness in Foundations

Gödel's proofs are invalid even though:
* The Peano/Dedekind categorical axioms for N are very powerful.
* It was Church/Turing who first gave a valid proof of the inferential incompleteness of N using computational undecidability.

The reason that Gödel's proofs are invalid is that they make use of a nonexistent fixed point to construct the "self-referential" sentence "I am not provable."

Mathematics is provably both open and inexhaustible.

Theorems of Mathematics can be generated but they cannot be exhaustively computationally enumerated.

See page 13 of Inconsistency Robustness in Foundations.

Theorems of Mathematics can be generated but they cannot be exhaustively computationally enumerated.

I was careful to confine my informal statement to just constructible theorems since you allow all reals to be used as terms.

Thomas,

Good point!

Cheers,
Carl

Mathematics is yet another very informal syntactic formalism. Therefore, everything you state about it is true; it's just letters on paper.

You can try to make things precise. Then you end up with either another syntactic formalism such as Z or Birds-Meertens, or you can try to fully formalize and mechanize it end you end up with a prover such as Lego/Coq/HOL/PVS.

I don't think mathematics exist, except for some vague agreed up notion as how to write symbols on paper.

Fixed points are mathematical objects. Fixed points do not exist in direct logic, therefore direct logic is not mathematics.

Although I do not doubt the underlying question. I think there is a formal language in which all of mathematics can be expressed, I just don't think it's direct logic.

I think what this language is like is an interesting question. At the moment I would say its something like Horn Clauses. A meta-logic in which we can write the axioms of mathematics and test them for consistency.

Obviously you could not prove the consistency of the meta-logic in itself (such a thing would be meaningless in any case) so the logic needs to be simple enough to be intuitively correct.

Fixed points are mathematical objects. Fixed points do not exist in direct logic,

Hewitt's assertion that "fixed points don't exist" is a description of a characteristic of a particular syntax. In the syntax of his system, there are no sentences containing self-encodings. A sentence-like-string containing a self-encoding is not part of any WFF.

You can still do Goedel's fixpoint constructions just fine, but only as meta-reasoning about systems being modeled. Basically, it becomes possible to state Goedel's theorems with a lot of formal precision.

I am thinking about things like Zeno's paradox. The fixed point of the infinite series 1 + 1/2 + 1/4 ... = 2. This is clearly part of mathematics, so any system that cannot express this is not "mathematics", but just another formal language. Hewitt's system may be consistent, but it is incomplete (hence not contra Godel).

With specific relevance to computing, Object instantiation is the fixed point of the record (see my post below).

Can Hewitt prove his system is complete (to be contra Godel it must be consistent and complete).

Further, if we observe that a required property of mathematics is that it is self-consistent, there is nothing that requires there be a single self-consistent system. There may be multiple possible "mathematics" each self-consistent, but not mutually compatible, kind of like independent mathematical universes. One could say that consistency vs completeness is obvious, if we try any be complete we necessarily have to include multiple incompatible mathematics into the whole, which results in an inconsistent system.

It is easy to see this in action. Heyting algebra and Boolean algebra both operate in the domain of single 'bit' values, yet they produce inconsistent results. You cannot have a single binary logic incorporating both, you have to choose the domain. Now we can introduce types to keep these separate, but then the types themselves can have different systems (extensional vs intensional type theory for example). So we can introduce a type-of-types, and so on to infinity.

I guess the real question is can we consider this infinite stack of types to be mathematics? Maybe this is what Hewitt is trying to say, that mathematics is by nature open and cannot ever be "complete", but it can be consistent. That seems reasonable, almost trivial, but does not contradict Godel.

So if Hewitt is saying that we use types to fragment mathematics in to self-consistent domains, such that consistency within a domain is a requirement, and that types keep domains separate, so that a Heytingean is a separate type from a Boolean, then the system is by definition consistent (but not complete). Q.E.D. Then I think I agree, but I don't see any necessity to ban fixed-points for this to be true.

The fixed point of the infinite series 1 + 1/2 + 1/4 ... = 2.

Hmm. 2 is the fixed point of a procedure \x.(1 + x/2). Hewitt says that can be expressed and proved.

Also that 2 is the limit of an inductively defined series 1, 1 + 1/2, 1 + 1/4, and so on. Yes, that can be proved too.

Can Hewitt prove his system is complete (to be contra Godel it must be consistent and complete).

Hewitt's formalization of math-in-general is "complete" this way:

Suppose you have a theory T such that T proves some proposition P:

T |- P.

In Hewitt's system you should be able to show:

|- (T |- P).

If T also happens to prove not(P), then in Hewitt's system you'd also get:

|- (T |- not(P))

Thus the inconsistency of T is demonstrated by those self-consistent theorems in Hewitt's system.

Hewitt's system contains the infamous trivial proof that it does not prove any proposition P and not(P). (No "|- P" and "|- not(P)".)

Goedel's second theorem shows a method for deriving a contradiction from a proof of self-consistency but Goedel's 2nd theorem method doesn't work in Hewitt's system. Goedel's method requires the target system to permit a sentence to be defined as a fixed point of a formula containing S itself. Type restrictions in Hewitt's syntax prevent any such function from being defined.

I guess the real question is can we consider this infinite stack of types to be mathematics? Maybe this is what Hewitt is trying to say, that mathematics is by nature open and cannot ever be "complete", but it can be consistent. That seems reasonable, almost trivial, but does not contradict Godel.

Goedel is often assumed to have killed off Hilbert's program from the 1920s. In 1927 Hilbert wrote the quote below. Goedel is commonly supposed to have shown Hilberts goal a lost cause:

It is a great honour and at the same time a necessity for me to round out and develop my thoughts on the foundations of mathematics, which was expounded here one day five years ago and which since then have constantly kept me most actively occupied. With this new way of providing a foundation for mathematics, which we may appropriately call a proof theory, I pursue a significant goal, for I should like to eliminate once and for all the questions regarding the foundations of mathematics, in the form in which they are now posed, by turning every mathematical proposition into a formula that can be concretely exhibited and strictly derived, thus recasting mathematical definitions and inferences in such a way that they are unshakeable and yet provide an adequate picture of the whole science. I believe that I can attain this goal completely with my proof theory, even if a great deal of work must still be done before it is fully developed.

No more than any other science can mathematics be founded by logic alone; rather, as a condition for the use of logical inferences and the performance of logical operations, something must already be given to us in our faculty of representation, certain extra-logical concrete objects that are intuitively present as immediate experience prior to in thought. If logical inference is to be reliable, it must be possible to survey these objects completely in all their parts, and the fact that they occur, that they differ from one another, and that they follow each other, or are concatenated, is immediate, given intuitively, together with the objects, is something that neither can be reduced to anything else nor requires reduction. This is the basic philosophical position that I regard as requisite for mathematics and, in general, for all scientific thinking, understanding, and communication. And in mathematics, in particular, we consider is the concrete signs themselves, whose shape, according to the conception we have adopted, is immediately, clear and recognisable. This is the very least that must be presupposed; no scientific thinker can dispense with it, and therefore everyone must maintain it, consciously, or not.

Subsequent to Hilbert and Goedel types became better understood.

Hewitt is (at least claiming, plausibly) to point out that Goedel did not kill Hilbert's program at all. In fact, Hewitt has a candidate system to do what Hilbert wanted.

That theory T is inconsistent means that there is some proposition Ψ such that

⊢T Ψ 
⊢T ¬Ψ 

Hilbert's program was not entirely well defined and somewhat more complicated than you indicated above.

Also, Hilbert would likely not have been happy with the Direct Logic proof of consistency although he was angry at Gödel for the incompleteness results.

OK (re notation).

Re Hilbert's program being not entirely well defined: That's why they thought it was incredibly hard.

Every time I start to think I see something useful here, something else comes along that just doesn't seem to make sense. One sentence seems full of insight, the next incoherent and random.

What does "|- T" mean? I can infer T from nothing? (I have read that part of the paper, and I know what it says it means, but I don't get how it can mean that).

It seems to me that there is a big self referential statement here, mathematics is consistent, and what is consistent is mathematics. The system which outlaws self referential statements is defined by one? Isn't that a paradox?

⊢_T Ψ means that theory T infers propositon Ψ .

What does "|- T" mean?

As Hewitt points out it means I created confusion by wrong notation. (re |-_T). Sorry.

Goedel's method requires the target system to permit a sentence to be defined as a fixed point of a formula containing S itself.

I am not entirely sure that is the case. Possibly you get it much better than I do.

I've been looking at when you cross the border from complete and consistent to complete or consistent. So, turns out Presburger arithmetic is consistent and complete. The difference seems to be that you shift from something which only has addition to something which has both addition and multiplication; which, by itself, I find a highly unsatisfactory observation (I would like to see explained another time.)

Don't you need fixed points to define addition? From a lambda calculus perspective, long time ago for me, I wouldn't see the difference between addition and multiplication that trivially. I would assume that if you would need a fixed point for multiplication then you would also need a fixed point for addition. (The latter implying incompleteness of Presburger arithmetic if the existence of fixed points in an LC possibly imply incompleteness a-la Godel.)

(It would be nice to see that in LC addition can be defined directly and for multiplication you need a fixed point, though, as another argument supporting Goedel informally.)

It's all nice, but getting rid of even addition?

EDIT: I guess I should have written something like "the fixed point isn't the problem, multiplication (or something like that) is." I.e., solving the wrong problem.
EDIT: Or: It's likely you need a fixed point to prove Godel's incompleteness results. But that's not the same as that you've proven you need a fixed point for a proof of incompleteness.

I am not entirely sure that is the case.

It's not. One way of thinking of diagonalization is that it operationally guarantees a fixpoint will occur (not that I've often seen the term "fixpoint" used for it in that context). It doesn't matter whether or not the occurrence can be talked about within a particular formalism.

It doesn't matter whether or not the occurrence can be talked about within a particular formalism.

Unless you are using Goedel's second theorem to try to produce a contradiction in an allegedly overpowerful, inconsistent system.

It's a theorem. It doesn't matter what you're using it for.

John, I think you are confused about Goedel's 2nd result:

It's a theorem. It doesn't matter what you're using it for.

The theorem has the form of a construction. The construction tells you how to construct a contradiction in certain over-powerful systems.

The construction can not be carried out in Hewitt's system.

There is no other way to appply Goedel's 2nd theorem to a system other than to use it to try to carry out the construction it proposes.

No, I'm not confused. You can take a look at my proof of the general result, if you like (pretty sure there's a link to it around here somewhere).

The Church/Turing inferential incompleteness theorem does not mean that consistency is unprovable.

I'll try and map for you:

Goedel, Church, Turing, many since prove that sufficiently powerful systems must be inferentially incomplete or else inconsistent.

Goedel proved that in some sufficiently powerful systems, a proposition asserting self-consistency of the system could be constructed in such a way that either that proposition could not be proved, or else a contradiction could be derived within the system.

Hewitt's system contains a proposition of self consistency and a proof for that proposition, but the proposition is not of the sort that Goedel needs to derive a contradiction.

Goedel's construction of the kind of proposition he needs is blocked in Hewitt's system, similarly to how you are blocked from creating a circular list structure in a pure dialect of lisp.

Types mean that fixed points don't exist for sentences; also they don't exist for propositions.

Consistency is possible for practical classical mathematical theories but not inferential completeness.

I am not entirely sure that is the case.

You are thinking of Goedel's incompleteness work as one theorem but we're really talking about two different ones here.

First:

Let us stand outside of a system X for a second and work with a model of X, Xm. In Xm let's assume formula and sequences of formula are encoded as numbers. So is a proof procedure for X (a way to check the correctness of a sequence of steps. Further, assume that X itself has enough "power" not to express "Xm encodes X" but instead just enough to describe Xm. Standing outside of X, you and I know by demonstration that Xm formulas can be translated back into X formulas. In X itself, by assumption at the moment, there is no way to prove that an encoded formula corresponds to its unencoded version.

Goedel's first theorem essentially gives us a computational method for producing an encoded sentence, Sm, such that we can be confident X can prove neither S or not(S), unless else X can prove both S and not(S).

X is therefore inferentially incomplete or else it is inconsistent.

We could create a new system, X+S, in which S is adopted as a new axiom.

In Hewitt's system we could treat S as an axiom in a new theory and continue on.

So far no problems.

Goedel's second theorem ponders what would happen in a system powerful enough that we didn't have to step outside it.

In other words, what if system X could itself prove that S is provable if and only if the encoded form, Sm, is "provable" in the Xm model?

Further suppose that, like Hewitt's system, X contains a theorem that says it X is consistent: "no S exists where S and not(S) are both provable".

Given that much, Goedel shows how to derive a contradiction in X. X would, in that event, be inconsistent. Roughly, "We just proved, using Sm, that S can not be proved. But S implies that S can not be proved. So S is true. A contradiction!"

You see: Goedel's second theorem is a kind of proof schema that can be adapted to attack any overly powerful (hence inconsistent) system.

For Goedel's attack-from-the-inside method to work, a system X has to permit a sentence S to be defined recursively. Roughly, "S is defined to be the formula Q with the encoding of S substituted for a certain of Q's terms." S is recursively defined in terms of its own encoding. S is a fixpoint of a function mapping sentences to sentences.

Hewitt says the type restrictions of his system prevent such a definition of S. I think roughly the restriction amounts to: You can construct sentences only from primitive terms and from earlier constructed sentences.

You can't form a sentence S that says "This sentence, S, is provable if and only if Sm has a model proof in Xm."

With that restriction, the attack vector of Goedel's second theorem, his method for deriving a contradiction in an inconsistent system, doesn't work. You could take this as empirical support for the claim that Hewitt's system is consistent.

Hewitt's larger argument "contra Goedel" is that Goedel was able to get away defining sentences by fixpoint that way only because of a confusion at the time. That, indeed, the syntactic restriction Hewitt proposes should be universal to all of math. Permitting self-referential sentences in any but a trivial system is, after all, a way to instantly make the system inconsistent!

The Second Theorem still doesn't require explicit self-reference. The "fixpoint" still doesn't have to be known by the formal system being studied. The formal system does have to do a bit of elementary reasoning, but nothing troublesome, other than the basic premise that the system proves its own consistency.

Technically, the First Theorem doesn't require explicit self-reference either. It's convenient to explain it as a sentence with a "this" in it to philosophers, but technically you have a simple relation R(x, "x"). (The mathematics doesn't have a concept of the noun "this".)

That's not weirder than any relation P(x, y), the quoting is weird but the self-reference doesn't exist. I think there's some discussion about it on the Wikipedia page but I am not sure.

The Second Theorem still doesn't require explicit self-reference.

Yes it does. Goedel wrote:

Theorem XI: [which we call the second theorem]: Let x be an arbitrary recursive consistent class of FORUMULAS. Then the SENTENCE which asserts that x is consistent is not x-PROVABLE; in particular, the consistency of P is unprovable in P, assuming that P is consistent [...]

[The proof is outlined, then....]

Now we establish the following: All the defined concepts (proved assertions) of Section 2 and Section 4 are expressible (provable) in P. For, we have used throughout only the ordinary methods of definition and proof of classical mathematics as they are formalized in system P. In particular, x (like every recursive class) is definable in P. Let w be the SENTENCE by which Wid(x) is expressed in P. [...]

The second theorem requires that the target system be able to define its own class of sentences (which Hewitt's does) and to construct a member of that class by fixpoint (which Hewitt's system does not permit).

Critical to the proof is that the target system is able to deduce from unprovability of an encoded statement in the model, the unprovability of the unencoded statement in the target system itself. If the target system can not do that, Goedel's attack doesn't work.

It's well-known (or at least I tend to think so, granting that in a wider sense none of this is well-known) that Gödel's original proofs were far more specific than the priciples they embodied; as I recall, he deliberately limited the actual proofs to PM to avoid accusations of abstract flimflammery. Whereas in my treatment I removed as many assumptions as possible in order to debunk claims that his results were somehow consequences of idiosyncratic assumptions in his treatment.

[note: imperfectly phrased, but the bottom line is right.]

Gödel's "proofs" were based on Principia Mathematica, which had types that are now corrected thereby clearly invalidating the "proofs".

Responding to Wittgenstein's critique (that "self-referential" sentences lead to inconsistency in mathematics), Gödel retreated to first-order logic (which has the bug that it can't categorically axiomatize N).

The crux is the premise of the second theorem that the system under question proves a certain consistency sentence, which we informally read as "the system proves its own consistency". The particular form this sentence takes matters a great deal.

In one sense, the second theorem surely applies to Hewitt's system: if his system (with his theory of naturals included, of course) could prove the canonical Gödel consistency sentence, or a consistency sentence satisfying conditions that have since been considered in order to generalize Gödel's result, then surely the system is inconsistent. (I agree with you).

In another sense, the second theorem doesn't apply, as we have no evidence that this premise is satisfied. In particular, Hewitt's "self-consistency of mathematics" is so trivial as to give us no a priori expectation that it qualifies as a strong enough consistency sentence. In particular, in order to make use of it, we would seem to be bound by the syntactic and type restrictions that are in place with the quotation mechanism it uses (Hewitt's syntax reflection). There's plenty of opportunity there to block a construction. (However, the last thread on this proved that it is actually subtle whether the construction is blocked). This is how I interpret what Thomas Lord is saying. (And I think I agree with him.)

Whereas in my treatment I removed as many assumptions as possible in order to debunk claims that his results were somehow consequences of idiosyncratic assumptions in his treatment.

If you are both correct and faithful to Goedel in consequence, then your cleaned up version of the 2nd result should provide us a recipe for constructing some specific propositions from which we can derive a contradiction.

Where can I see your recipe for performing a construction in a target system?

A pattern in Hewitt's arguments is treating Gödel's results as if they were anomalous consequences of some pathological assumption, so that some minor disruption of the particular assumption can cause the basic result to fail. That's unrealistic; as some of us have pointed out from time to time, the reason Gödel is famous is that the principles involved are stunningly robust. These particular treatments are just parts of the elephant. I did try for a somewhat larger part of the beast, but I suspect it's still only a small part compared to the whole. For what it's worth, the part of the elephant I've been looking at is described in my blog post (I was right, there is a link to it eleswhere in this discussion) "Computation and truth".

The Church/Turing proof of the inferential incompleteness theorem is robust; but Gödel's arguments fail because fixed points don't exist.

Chaitin [2007] presented the following analysis:

Gödel’s proof of inferential undecidability [incompleteness] was too
superficial. It didn't get at the real heart of what was going on. It
was more tantalizing than anything else. It was not a good reason for
something so devastating and fundamental. It was too clever by half.
It was too superficial. [It was based on the clever construction]
“I'm unprovable.” So what? This doesn't give any insight how serious
the problem is.

The deeper reason for inferential incompleteness is given by the Church/Turing proof.
Gödel’s argument for the 1st incompleteness theorem was based on the pathological assumption that fixed points exist.

A pattern in Hewitt's arguments is treating Gödel's results as if they were anomalous consequences of some pathological assumption, so that some minor disruption of the particular assumption can cause the basic result to fail.

It's really not. He's saying something really simple in this area but it is evidently hard to communicate simply.

If I may I refer you to the "proof sketch" comment I very recently made to marco on this topic page. It might shed some light.

Still unconvinced one needs fixed points for the construction of Godel's argument.

Still unconvinced one needs fixed points for the construction of Godel's argument.

That's on you.

Of course not. You claim one needs a fixed point to express certain constructs. But when I look at, what I expected would usually be recursive constructs, addition and multiplication of Church numerals, I find they are easily expressed without recursion.

What is to say that this isn't true in the general case?

In order for the proposition "By forbidding fixed point combinators Godel's argument doesn't hold" to be true, the burden is on you to prove that fixed point combinators are required for his proof.

Maybe it's true, maybe it isn't. But I am not the one who is stating that by ruling out fixed point combinators certain arguments don't hold anymore.

(Formal explanation of your argument: """So you know when you go down town with the lads and you all realize you’re hank marvin’ so you say “lads let’s go Maccers” but your mate Smithy a.k.a. The Bantersaurus Rex has some mula left on his nandos gift card and he’s like “mate let’s a have a cheeky nandos on me” and you go “Smithy my son you’re an absolute ledge” so you go have an extra cheeky nandos with a side order of Top Quality Banter.""")

(Hewitt is the Bantersaurus Rex/Smithy in this case.)

Of course not. You claim one needs a fixed point to express certain constructs.

No, I don't claim that. Goedel does.

Goedels second result shows how to construct, within a system, a sentence that is either unprovable, or that produces a contradiction. In this construction, the sentence implies the consistency of the system itself by asserting the non-existence of any proposition for which proofs of the proposition and its negation both exist.

A stated condition of the construction is that the system must permit you to construct new sentences by arbitrary recursion. Goedel offers no alternative construction without this. Nobody else ever has either. As I said: if you think there is one, that's on you. It's your burden.

Meanwhile, sentences in Hewitt's system can not be defined by arbitrary recursion and Goedel's construction can't be applied. Hewitt's system can separately prove its own self-consistency, but Goedel's construction can't be used to derive a contradiction.

Maybe some orignal construction, very different from Goedel's, could derive a contradiction in Hewitt's system. You never know. Consistency is ultimately an empirical question for all systems. But we do know that Hewitt's can prove its own consistency, Goedel's construction can't be performed in Hewitt's system, there is no contradiction there, and in retrospect you can see what Hewitt means with his critiques of Goedel and other earlier mathematicians working in this area.

A stated condition of the construction is that the system must permit you to construct new sentences by arbitrary recursion.

And where does Goedel use an Y combinator in his construction exactly? And how is the construction of new sentences fundamentally different from superficially arbitrary recursive construction of numbers by addition or multiplication?

At least with the shift from Presburger arithmetic to an incomplete arithmetic a-la Goedel by adding multiplication there's a minimal hint where something starts to break.

Instead, you've seemed to have invented an arbitrary side condition which, if you rule it out, would prevent Goedel's argument. That's just your imagination.

You invented the side condition and therefore you need to prove it. Even if it is likely true. Likely isn't good enough.

And where does Goedel use an Y combinator in his construction exactly? And how is the construction of new sentences fundamentally different from superficially arbitrary recursive construction of numbers by addition or multiplication?

In the first theorem, the apparent recursion can be eliminated. In the second it can not.

To make this clearer, I will paraphrase Goedel's sketch of the first proof, using a particularly good translation (linked below), and then elaborate with respect to the second incompleteness result.

Let R_n be an ordered list of sentences with one free variable. (Goedel calls these "class signs".)

Let R_n(x) be the sentence formed by substituting x for the free variable in the nth class sign.

K is a class of natural numbers:

K := { n in Nat.| ~ Provable (R_n(n)) }

In that way, K is a class of numbers such that the nth class sign, with the free variable replaced by n, is not provable.

Now we define S, a class sign. For some q, S is R_q

S == R_q

What is S specifically? Which "q"? S is:

S(n) := R_q(n) := n ∈ K == n ∈ { k in Nat. | ~Provable(R_k(k)) }

Goedel's famous sentence is:

S(q)

Either S(q) can not be proved, or the system is inconsistent.

S(q) <=> q ∈ K <=> ~Provable(R_q(q)) <=> S(q) <=> ~Provable(S(q))

Goedel's second result requires us to make a definition like this in
the target system:

X := S(q)

equivalently:

X := R_q(q)

equivalently:

X := q ∈ K where (X == R_q(q))

Suppose that X is provable in the system where it is defined.

Then within that system we trivially get:

~(q ∈ K)

but the proof of X gives us:

(q ∈ K)

so we have a contradiction.

In Hewitt's system, this definition:

X := q ∈ K where (X == R_q(q))

is ruled out.

http://www.ursuletz.com/cs150-fall2005/lectures/goedel.pdf

Thomas,

In Direct Logic, sentences are not countable because they can contain real numbers. However, strings are countable.

Also, sentences are different from propositions (which do not contain free variables.)

Consequently, Gödel's argument for the 1st incompleteness theorem fails. However, the Church/Turing proof of the 1st incompleteness theorem is valid.

In Direct Logic, sentences are not countable because they can contain real numbers.

I think you refer to Goedel's use of of the well ordered set R_n, a set of formula containing a single free variables.

The set R_n does not need to include all formulas with one free variable for Goedel's proof to work. It can include only, say, a specific and easily laid out countable set that can be inductively defined. (Which he more or less does in the the details for PM.)

Also, sentences are different from propositions (which do not contain free variables.

In all of these comments I am being loose with terminology rather than strictly adhering to yours. I might try to switch later but right now I'm just trying to help people better intuit what's going on here.

Consequently, Gödel's argument for the 1st incompleteness theorem fails.

I think you are mistaken there in the sense that we can formalize his first argument well enough to apply it to a partial syntactic model of your system.

In Direct Logic, fixed points on propositions do not exist and consequently Gödel's proofs are not valid. Even in the closed theory ℕ, a “self-referential” sentence cannot be constructed by enumerating strings for sentences. Let SentenceFromStringWithIndex be a procedure that enumerates sentences that can be produced by parsing mathematical strings of the closed theory ℕ and IndexOfSentenceFromString be a procedure that returns the index of a sentence that can be obtained by parsing a mathematical string.

I_am_not_provable:Proposition ≡ ⌊SentenceFromStringWithIndex.[Fix[Diagonal]]⌋ 
    where  Diagonal.[i:ℕ]:ℕ ≡ IndexOfSentenceFromString.[⌈⊬ℕ ⌊SentenceFromStringWithIndex.[i]⌋⌉]

Because of types in Classical Direct Logic the fixed point operator Fix cannot be defined because of the following:

 
   ℕtoℕ ≡ [ℕ]↦ℕ
   Helper.[f:ℕtoℕ]:ℕtoℕ ≡ [x:([⍰]↦ℕtoℕ])]→ f.[x.[x]]
   Fix.[f:ℕtoℕ]:ℕtoℕ ≡ (Helper.[f]).[Helper.[f]]

The missing type ⍰ does not exist.

In Direct Logic, fixed points on propositions do not exist and consequently Gödel's proofs are not valid.

Goedel's metamath demonstration in the 1st incompleteness theorem doesn't deeply rely on treating propositions of the target system as first class objects. It can operate entirely on a model of the target system.

The judgement that the model is faithful to the modeled system is not a formal judgement.

Gödel's argument for 1st incompleteness theorem requires a fixed point.

Gödel's argument for 1st incompleteness thm requires fixed point

Yes, but it can effectively compute the needed fixed point using the integer encoded forms of things. The structure of the argument in the 1st, as I read it, doesn't require any formal proof that the encoded form faithfully encodes the subject system. We're supposed to believe that the encoding is faithful by direct apprehension.

It doesn't matter much. The substitute version using ChurchTuring in DL is considerably more elegant, not least since it lacks the need for an encoding.

Because of types, sentences do not have fixed points.

Also, creating some of the sentences from strings does not give them fixed points.

One of the defects, imho, of the way Gödel's Theorems are usually treated, is an obsessive focusing on particulars of the formal system. When explaining why the halting problem is undecidable, one doesn't get into details of how particular machines work; so if Gödel's results are comparably fundamental one oughtn't have to mess with nitty gritty technical details either. That was part of what I wanted to explore in my blog post. As I pointed out there, at the time it was all thought of as a matter of tinkering with rules of deduction and axioms, so it makes sense one would concentrate on those things, but in retrospect it doesn't seem to be about rules of deduction or axioms at all, in fact it seems to be mostly independent of those things. By the time I'd finished going through it all, I was fairly satisfied that it is, indeed, possible to get at the basic results without having to resort to things like the Law of the Excluded Middle, or reductio ad absurdum. I wasn't even bothering to look for fixpoints, which I wouldn't have expected to find, but since it's been brought up here, I observe that there's nothing like that going on either. Except that in any treatment of the Second Theorem it's hard to see how you can avoid getting into a little of the behavior of the system; not very much, and probably there are lots of different specific choices of what exactly to require, but something. At the very least, you need to be clear on what you mean when you say the system "proves its own consistency".

Unlike Gödel's results (which depend on the existence of fixed points for sentences that don't exist because of types), the Church/Turing proof of inferential incompleteness is robust:
*Church first proved incompleteness using the lambda calculus
*Turing then proved incompleteness using Turing Machines

John, I have read the Goedel sections of your blog post.

The first error it contains is here:

Gödel's Theorem (aka Gödel's First Theorem) says that any sufficiently powerful formal system is either incomplete or inconsistent — in essence, either it can't prove everything that's true, or it can prove things that aren't true.

The first incompleteness result shows that any sufficiently powerful system either:

1. allows assertions to be made which it can neither prove or disprove

or

2. the system allows assertions to be made which it can both prove and disprove.

This is different. We are being more careful here to talk about assertions and formal proof within a system, rather talking vaguely about truth.

Another very critical mistake in your blog post is here:

Gödel's results are commonly phrased in terms of what a formal system can prove about itself, and treated in terms of the rules of deduction in the formal system.

Goedel's results pertain to formal systems and their proofs, that much is true.

Goedel's second result is commonly stated in terms of what a formal system can prove about itself because that is what the second result is concerned with.

Goedel's first result is never stated in terms of what a formal system can prove about itself because that is not what it is concerned with.

The types in Hewitt's system are used to avoid falling into a trap that Goedel's second result shows exists.

You say:

I phrased myself in terms of what we can know about the system — regardless of how we come to know — rather than what the system can prove about itself.

By implication, you have no interest in or anything to say about the second incompleteness result.

Inventing nonsensical misreadings of what I wrote as an excuse for claiming it's wrong is the sort of pettiness I'd expect of Hewitt. I honestly thought better of you.

I honestly thought better of you.

Suddenly, likewise.

Do you understand why we might expect Hewitt's DL self-consistency proof to invoke suspicions DL is inconsistent, based on Goedel's 2nd theorem?

Do you understand how Goedel's 2nd theorem does not automatically apply?

Do you understand how Hewitt proposes to prevent it from applying?

I am not asking if you accept that Hewitt has got it right or not. I am asking if you understand what he claims to argue.

From your blog account of Goedel it is genuinely unclear.

I understand this stuff reasonably well, yes (though your third question is quite different since it introduces Hewitt into the equation).

I've finally, btw, got a somewhat-plausible hypothesis for what went wrong with your reading of my blog post. More than half my fault. I gave you a link into the middle of the thing. Should have pointed you to the start of the post; I forgot that the earlier parts of the post are probably needed context if the reader is to understand what I'm doing (it's possible some people still won't connect with what I'm doing, but lacking the context would be a serious disadvantage). Though I admit, that only explains your first two-out-of-three remarks; it was always the third one that I found really objectionable, since it quotes a statement about form and then turns around and interprets it as if it were an absurd statement about substance.

Do you understand why I no longer take Hewitt's unsubstantiated claims seriously? Once upon a time we were both (so it seemed) operating on the assumption that Hewitt had some possibly-interesting ideas that he wasn't communicating well, and it seems you've continued to operate on that assumption; but he slowly expended all his capital with me, and I finally concluded that, by Occam's Razor, by far the simplest and therefore most likely explanation for his behavior over time would be that he lacks basic understanding of the subject.

That said, I still take you seriously, and if you say there's something interesting in Hewitt's recent writings, I'm willing to take a look (in my copious free time). Which paper did you have in mind?

Which paper did you have in mind?

Inconsistency Robustness in Foundations: Mathematics self proves its own Consistency and Other Matters

I like this quote:

The development of Direct Logic has strengthened the position of working mathematicians as follows:
 Allowing freedom from the philosophical dogma of the First-Order Thesis
 Providing a usable type theory for all of Mathematics
 Allowing theories to freely reason about theories
 Providing Inconsistency Robust Direct Logic for safely reasoning about theories of practice that are (of necessity) pervasively inconsistent.

I'll take a look when I get a chance, and offer my thoughts on it here; then, at least, we can compare/contrast our reactions to it, which may be interesting to us (regardless of what Hewitt thinks of it). I suspect the last time I looked at that one wasn't so very long ago, but, we'll see. The passage you quote doesn't exactly inspire me with confidence, since high-level claims are something he's never been short of.

Apparently you feel insulted and I don't wish that you do.

Skimming a few pages from a most recent version of one of Hewitt's endlessly revised links, some of the introductory language seemed clearer to me and a bunch of stuff just clicked. In concept, Hewitt's system is butt simple but with plenty of tricky details to be careful to get right.

One way you could describe is that he has specified a kind of semantic tower of formal theories with a single, simplistic theory at root.

The tower comfortably admits inconsistent theories without any risk of contagion of inconsistency to sibling or cousin theories or any ancestor theory.

None of the theories, including the root theory denoted by the unsubscripted turnstile, admit the kind of self-referential trap Goedel described in his 2nd incompleteness result (part 4 of "On formally undecidable...").

Via its sub-theories, which are all first class object about which it can reason, the root theory appears to admit all classical mathematics. For example, you can keep generating new arithmetic axioms by diagnonalization arguments for the rest of your life and DL can keep incorporating them as axioms in new sub-theories.

At least from the earlier part of the post that I absent-mindedly led you to bypass, it should be evident that what I'm interested in is the broad principles involved. On the First Theorem, I maintain that the broad principle involved does in fact concern completeness in the sense of external truth. Note, though, that the only external truth we actually need for the proof is the truth acquired by the reasoning in the proof, which is to say, the meta-mathematics of the proof. The advantage of acknowledging that we care about the meta-mathematics only on the grounds that it's true is, that it highlights our disinterest in details of the system whose properties are being studied. That disinterest is part of why tactics of the ilk Hewitt has been advocating (at least, those he's been mentioning here; yes, I'm going to take a fresh look at the paper you recommended) don't advance the cause of avoding the broad principle.

Precision and rigor are important in the foundations of Computer Science both for broad principles and in detailed technical arguments in order that computer computer systems can carry out all reasoning processes.

That Gödel's incompleteness arguments are invalid is important because otherwise we would have inconsistencies in the mathematical foundations of Computer Science.

[wrong thread]

Science is always a work in progress.

The powerful (try to) insist that their statements are literal
depictions of a single reality. ‘It really is that way’, they tell us.
‘There is no alternative.’ But those on the receiving end of such
homilies learn to read them allegorically, these are techniques used
by subordinates to read through the words of the powerful to the
concealed realities that have produced them.
Law [2004]

God man. They already asked me once to write a prover for an inconsistent system once during my PhD studies. I flat-out refused.

I don't do mysticism. Clean up your mess or go packing.

Comments and suggestions gratefully appreciated for the articles on HAL.

Thanks!
Carl

That Gödel's incompleteness arguments are invalid is important because otherwise we would have inconsistencies in the mathematical foundations of Computer Science.

So what. This is simply likely true. I am not bothered by it.

Gödel implies that if you try to reason over numbers, it turns out you can't. So, either our reasoning or our numbers are flawed.

Personally, I am betting that the numbers are flawed. Life might be just that, continuous. Panta rei, everything flows, all else is a cosmic joke.

Still. Classical higher-order logic reasoning works 99.99, and then some, of the time. It's effective, we haven't found primes which are dividable by other numbers yet. There's only that one Gödel sentence.

I still think it's just a nice joke though.

The Peano/Dedekind categorical axiomatization of N is not flawed.

Furthermore, inconsistencies in mathematical foundations of Computer Science are not a joke because they can lead to security holes :-(

"they can lead to security holes"

https://xkcd.com/704/

It's unlikely you can deduce my mother's phone number from 1=0 ;-)

Godels result is always lingering there over you in the meta-logic. The logic you use to reason over other systems.

Personally, I think Godel tells us that we tried to discretize a continuous system and that works great, except for in the limit. Numbers don't exist in nature, you saw two blobs in a vague picture and thought you could assign two-ness to it. Well, you can, works 99.99% of the time, but Godel tells us that mode of thinking is fundamentally flawed.

So you end up reasoning in an inconsistent system where your results are invalid in the limit. Godel might have found an inconsistency in an inconsistent system and the whole Godel sentence might not even exist. Valid reasoning but inconsistent system.

That doesn't need to be bad, might not have implications for security holes. There simply are modes by which you can brute-force problems, do some finitistic reasoning, or keep it that simple that it looks true to you.

That's my 2cts on it.

I would say does not have implications for security holes.

It sounds like bullshit.

My reading of Godel is that Godel fundamentally tells us that the universe is a continuum, cannot be understood, and that our discretization of that continuum is an effective, but flawed nonetheless, endeavor.

Contrary to Hewitt I am not here to claim that's anything correct, mind you. It's just a believe I am stuck with concerning the relation between human thought and reality.

So, if you find that bullshit, that's okay with me.

But Hewitt is right in that it has implications for security holes. If all logic is inconsistent, then it follows that you cannot prove security protocols correct in the limit.

Personally, I would say that as long as you steer away from constructing Godel sentences, you're in that 99.99, and then somewhat, percent effective region, and it simply doesn't matter much.

But it's just an odd belief.

reasoning about discontinuous finite things with defined and limited operations.

The fact (?) that the universe is continuous doesn't enter in at all.

As far as I can tell, discrete math is not threatened by this bullshit at all. Valid proofs about finite systems are not threatened at all.

In fact if you want to make proofs about computer systems, then I would say, start with a system that uses no uncountable infinities because you don't need them in the slightest.

Depends on what you understand what discrete math is. Godel tells us that systems which can reason about arithmetic and are sufficiently strong are not both consistent and complete and cannot state their own consistency.

So now we know there are (likely many) things you can state about numbers which cannot be proven.

They have proven Godel correct in Nuprl?, Coq, and lately Isabelle/HOL.

These are mechanical systems in which mathematical theorems and also protocols are verified. It would be nice if it had turned out that these systems are trustworthy beyond doubt. The proof of Godel seems to tell us that they are not beyond doubt; so you need an answer for that somewhere.

Uncountable finities are somewhat of a byproduct of the current discussion with Hewitt. I would say that he didn't make it better, but he made his position worse; not only is there still doubt about the discrete part of his logic, there's now also doubt about how he treats infinities and infinitesimals.

We're in a deep mess already without starting on the topic of infinities.

Say that "sentence" is something that can only talk about N bits and no more and that "sentence" can't be more than M symbols long.

Now we're talking about something like a computer system and programs.

Does Godel apply here? I doubt it.

This is simply likely true. I am not bothered by it.

Although I agree with your indifference to Gödel's results being true, I point out that it's not true those results would require inconsistencies. They require a formal system to be either inconsistent or incomplete. But yes, that's not a big deal; as I remarked in my blog post on this stuff, the impossibility of a formal system being both complete and consistent is just a characteristic of formal systems, rather like it's a property of Euclidean geometry that a triangle can't have more than one obtuse interior angle.

I can't follow this discussion so I'm curious what's your opinion of how it hashed out.

Did Hewitt impress anyone with his proposed foundation?

Is Godel important?

Is it true that fix points can be banished from math without diminishing it, sort of like replacing infinitesimals with limits?

Is banishing fixed points throwing the baby out with the bathwater, a bit like banning division instead of banning division by zero?

I was a bit taken aback to realize that you all were saying that mathematical statements aren't countable which means nothing more than that you're allowed to make statements about real numbers :/ That sounds utterly useless.

Is there any THERE there?

Is there a logic which is actually more usable and correct in practical computations or has CS gained nothing useful yet from all of this?

[edit] I was aiming this question at John Shutt. Also I realized after I posted it, there is another way to get to uncountable sentences than embedding elements of the continuum in otherwise finite sentences, there is also taking power sets of countable infinities of sentences. It occurs to me that no human is going to invent a proof whose Kolmogorov complexity requires an infinite basis. Ie if you can't describe a proof in a finite amount of time, then no human will reason about it. Even if you can show that you are meta-reasoning about such objects, you should also note that it's useless - no such object will ever have meaning to a human being.

Beyond that, they're talking about Actors being uncountable. Uhm so they're not talking about computer science at all anymore.

Have they taken a model for computation and turned abstracted it into some other sort of mathematics or is this whole conversation getting confused?

An actor that isn't a finite series of steps with finite data is at best some sort of abstraction that isn't in computer science. If you are including infinitely long computations like comparing reals or members of infinite sets, at best you're into hypercomputing, which I imagine is in general more disreputable than "fixed points" but which is ok as mathematics if not computation. But maybe those things could be a replacement for "fixed points" a spot in mathematics to be suspicious of. We can take or leave the axiom of choice... If we're only allowed countable infinities or no infinities at all, then all sorts of paradoxes disappear.

Meh I shouldn't talk about what I don't understand.

But what is this? Uncountable sentences? Those aren't mathematics as humans do. Uncountable actors? Those aren't, in general, programs that we can reason about let alone run. What is going on here?

Gödel's work is important because he first published on inferential incompleteness although his proofs are invalid. Church/Turing first published a valid proof of inferential incompleteness for Peano/Dedekind categorical axiomatization of N.

Fixed points do not exist in logical foundations of Mathematics without loss of power, which is fortunate because existence of fixed points leads to inconsistencies in Mathematics.

Strings are countable although for generality, sentences and propositions are not countable.

Types provide foundations for Mathematics that are much more powerful than first-order logic.

For details, see Inconsistency Robustness in Foundations

Is it possible that only a certain, tiny subsets of fixed points lead to inconsistencies and that the best answer is to analyze what it is about those fixed points that make them problematic rather than throwing out fixed points?

That sounds to me more like how mathematics progresses.

Did Hewitt impress anyone with his proposed foundation?

I am quite impressed. I came to this state of being impressed (and even able to explain some of it to others) from an earlier state of thinking it was nutty rambling.

I don't have anything to add here to what Hewitt said about Goedel and fixpoints.

The utility of uncountably many abstract mathematical sentences arises in the context of fully automated machine reasoning in which we can generalize the terms of sentences in certain ways.

But also from the other side: the generalization of pure math to include this concept also tames awkard foundational issues that college curriculums heretofore sidestep because they had no worked answers. I mean this quite literally. I had some of the best math instructors and program anywhere as an undergrad and even those guys were quite *explicit* that they were sweeping certain foundational questions under the rug because they didn't have a satisfying way to answer them. They "knew" by feel what kinds of reasoning were safe and where dragons could lay -- but they couldn't lay down a foundation to make that sense rigorous.

They could have done foundations for that curriculum with Hewitt's DL and little bit about Actors (in the mathematical abstract).

Is there any THERE there?

The comments on this LtU topic are only scratching a part of the surface. Wait till it comes around again how this relates to pervasively inconsistent networked information systems.

Thanks Thomas!

There are indeed deeper issues to be addressed in inconsistency robust logic.

Unless you're building sentences from elements of the continuum I can't imagine how you claim that sentences are uncountable.

And I can't think of any utility to sentences made from actual reals except that they're valid... Can't they replaced by sentences with symbols in the place of reals and some sort of statement to the effect of "there are reals for which this is true"

[Edit] I suppose you could take the power set of countably many sentences to make uncountable sentences. Once again I can't see any utility. And you could banish that by leaving out an unrestricted axiom of choice

[2nd edit] Ok I can imagine a proof that used a power set of sentences. ... So I guess I have to grant the possibility of a mathematics that has uncountable sentences, but such sentences could be reasoned about but not even a single sentence from the greater set could be examined!

[3rd edit] For CS, it would seem to me that programs aren't infinite, perhaps sentences that are members of the continuum aren't so relevant.

pervasively inconsistent networked information systems.

I don't believe this will relate to anything relevant to computers in my lifetime.

"The utility of uncountably many abstract mathematical sentences arises in the context of fully automated machine reasoning in which we can generalize the terms of sentences in certain ways."

But I am tempted to ask, you DO realize that merely generating infinite numbers of sentences can't get you to uncountable infinities. Unless there is a power set of an already infinite set (as you use to generate reals) then you don't have an uncountable set.

So where does automated reasoning need power sets of infinite sets of sentences?

Uncountablity comes from the type Boolean^ℕ.

Note: I told Thomas Lord I would take a look at the updated document of Hewitt's when I had a chance. I still mean to. I'm not looking forward to it; I suspect it's not really changed from the last time I looked at it. But I take Thomas Lord seriously enough to do that, even though Hewitt has slowly lost my respect over time.

That said, from the accumulation of what I've seen said here, and various occasions in the past when I've examined various of Hewitt's papers, there's no there there.

Infinities cannot be completed; if they could be they wouldn't be infinite. Perhaps we can reason indirectly about things that are not finite; for example, the decimal representation of an irrational number is itself infinite but we can describe it by giving an algorithm for enumerating its digits, and then use that to reason about it. How far can one go in reasoning about such things? Well, it's certainly possible to go too far. When you treat things that don't exist as if they do exist you can get into serious trouble. For example, a man in a village who shaves all men in the village who do not shave themselves, or the set of all sets that do not contain themselves. Every unicorn has one horn; but also, every unicorn has two horns (also five horns), and if you suppose that unicorns exist, you can therefore conclude that one is equal to two, and that's not going to end well. It was recognized way back that infinities are problematic; if they exist at all, one has to be careful how one reasons about them. Reasoning is itself finite, and so if we're to reason about infinities we have to do it starting from a finite foundation. Building infinities into a system of reasoning makes it unsuitable as a foundation, as it becomes something that needs a foundation under it in order to legitimize it.

ℕ is countable. ℤ is countable.

If programs are finite sequences of instructions then they can't generate an uncountable set.

Just because you can generate some numbers that aren't rational numbers with a finite program doesn't mean that you can generate ALL of them. The number of finite programs that have a finite amount of data is countable therefore the number of elements you can represent with a one to one mapping of such is countable.

If you had an uncountable number of actors then the address of any actor would take an infinite amount of memory.

The number of actors whose address is finite is a countable set! Therefore you can't have an uncountable set of actors with finite addresses.

These people don't seem to understand as much about Cantor as the average internet crackpot.

Also, mathematics may treat SOME VERY LIMITED set of kinds limits as completed, but if you treat general computing, the output of any system of actors as completed when infinite, then what they hell does that imply? Something monstrous! Something interesting but as far as I know never analyzed.

Actor addresses are uncountable, e.g., for a countable list of addresses of Actor reals, there is an address for an Actor that is not in the list.

:/
And you can't have an uncountable number of actors that are distinct NOT COUNTING THEIR ADDRESS unless they have infinite memory and or instructions too.

And there is no point in infinite instructions or infinite number of even finite memory if programs take finite time.

This is a very odd system indeed.

ℂ, ℍ, and ℝ are uncountable.

At given point in time, a physical machine will have a finite number of Actors.

The Peano/Dedekind categorical axiomatization of N is consistent but inferentially incomplete because there are true but unprovable propositions for N.

[...] this definition:

X := q ∈ K where (X == R_q(q))

Even if that were a recursive definition, it was given after two non-recursive definitions of X as a way to clarify their ramifications. You only have to pick whichever definition you're willing to believe, and the other two can be informal.

But look closer: It's not a recursive definition at all. It's just the definition "X := q ∈ K" and there happens to be a reminder "X == R_q(q)" meaninglessly tacked onto the side.

But look closer: It's not a recursive definition at all. It's just the definition "X := q ∈ K" and there happens to be a reminder "X == Rq(q)" meaninglessly tacked onto the side.

For the second incompleteness theorem to work, you have to produce (in the system itself) a proof that:

X = q ∈ K where (X = R_q(q))

You can't make that proof without a recursively defined formula. The particular recursive definition I gave for X is just one example of how you could do it (but that is not allowed in Hewitt's system).

You can't make that proof without a recursively defined formula.

Why not? I think Gödel didn't use one.

The particular recursive definition I gave for X [...]

When did you give a recursive definition for X?

I think Gödel didn't use one.

How else do you possibly make sense of section 4 of his paper?

It begins on page number 69, PDF page number 72 of this:

[update: sorry, forgot the link. here.

http://jacqkrol.x10.mx/assets/articles/godel-1931.pdf

]

Pay particular attention to the paragraph that begins "We now establish the following: All the concepts defined (or assertions proved) in Sections 2 and 4 are also expressible (or provable) in P." Especially footnote 67.

How else do you possibly make sense of section 4 of his paper?

I can't say I do make complete sense of it, and I'm sorry for that. There's a good chance I'll say something that I'll regret later.

67: That the correctness of w Imp (17 Gen r) can be concluded from (23), is simply based on the fact that—as was remarked at the outset—the undecidable proposition 17 Gen r asserts its own unprovability.

All propositions assert their own truth, but that doesn't mean we need fixpoints to construct every proposition.

Proposition 17 Gen r does in some sense assert its own unprovability, in the sense that it's logically equivalent to a (separate) statement that asserts the unprovability of that sentence. That's even how it's designed, but that's not how it's defined.

When did you give a recursive definition for X?

Without that or another fixpoint equivalent, you can't draw out the implications Goedel sketches in part 4.

The inferential leap you need, within the system, is from a theorem about the model to a theorem about a modeled statement. That's the big sticking point that doesn't work in Hewitt's.

When did you give a recursive definition for X?

Without that or another fixpoint equivalent, you can't draw out the implications Goedel sketches in part 4.

What are you referring to by "that"? I said "when," not "why."

Sorry for the confusion. In the comment with the subject line that begins "proof sketch...".

The following is a recursive definition of X.

X := q ∈ K where (X = Rq(q))

Here is a kind of schema for an assertion, with a free variable X (using earlier defined K and R_q):

q ∈ K where (X = Rq(q))

A definition of a sort, which Goedel was talking about, tries to bind the free variable to the whole assertion itself:

X := q ∈ K where (X = Rq(q))

It could as well be written something like:

letrec X := q ∈ K where (X = Rq(q))

To actually put a definition like this into a hypothetical formal system, some meaning has to be given to the assertion. The meaning Goedel relies on is a fixed point meaning. The meaning is something like the assertion

q ∈ K where ("this assertion iself" = Rq(q))

There might be more than one possible q. We might pick in particular a least fixed point using the well ordering of integers.

This is an assertion, something like a Sentence in Direct Logic, but to use the trick in Goedel's 2nd incompleteness theorem, the sentence must be overtly self-referential. It must be defined as a fixed point (which DL doesn't permit).

The following is a recursive definition of X.

X := q ∈ K where (X = Rq(q))

I guess we didn't connect when I said

It's not a recursive definition at all. It's just the definition "X := q ∈ K" and there happens to be a reminder "X == R_q(q)" meaninglessly tacked onto the side.

When I look at the definition of q and the definition of K, I think "X := q ∈ K" is already equivalent to the other two non-recursive definitions.

The part that says "where (X = R_q(q))" is just some extraneous clarification. All it does is call to mind the alternative definition "X := R_q(q)" from two lines ago.

If you're right and X is defined as "q ∈ K where (X = Rq(q))" then what does "where" mean here? If it establishes a local binding for X, then it's extraneous, since the expression "q ∈ K" contains no occurrences of X. If it establishes a second binding for the same variable X, then we have some kind of multi-valued definition, not a recursive one.

In a more recent thread, Thomas Lord said

Looking back at the earlier thread, you looked at this notation and said it was not a recursive definition... you say that there was no fixpoint here:

X := q ∈ K where (X = R_q(q))

The fixpoint semantics of this definition are the only thing that give q and X a specific meaning. Do you not see that X is defined in terms of itself there? That is is not some arbitrary q from the set K but is instead a very specific example of q in K?

The variable q was already defined elsewhere in your post above:

What is S specifically? Which "q"? S is:

S(n) := R_q(n) := n ∈ K == n ∈ { k in Nat. | ~Provable(R_k(k)) }

Unfortunately, that line is potentially even more confusing than the one we're already talking about. I'll unpack it. It's two definitions and an observation:

q := the i such that (R_i(n) == (n ∈ K))

S(n) := R_q(n)

Observe that (n ∈ K) == (n ∈ { k in Nat. | ~Provable(R_k(k)) }).

Now when the post gets around to the particular definition of X we're arguing about (and not the other two definitions of X)...

X := q ∈ K where (X == R_q(q))

...this line is defining X as the proposition "q ∈ K." It's also observing that this is the same as saying X is R_q(q).

[Updated: Ross Angle pointed out a mistake in the definition of ParadoxFormua_i which has been fixed (hopefully). The mistaken version can be seen in his comment below.]

I agree that my earlier description, which you quote, is sloppy.

I will try to make amends here.

We hypothesize a formal system for which we metamathamatically have a family of formulas indexed by natural numbers:

  Iformsi in ℕ
     an as yet undescribed set of formulas, indexed by naturals

What are these formulas? Each one has a free variable which, for our discussion, we may consider to be of type ℕ.

Notationally,

  Iformi(n)   where n ∈ ℕ
    is the sentence formed from Iformi by replacing the free variable with n

Metamathmatically speaking (for the moment), "Iform_i(n)" is a name for some sentence in the subject system.

(Incidentally, the "subject system" that we are studying metamathematically is already not Direct Logic because DL "formulas" are not countable. They can't be indexed by ℕ. But that isn't really central to showing how Goedel uses a fixed point so I'll move on from that.)

Goedel also assumes that proofs in the subject system can be indexed by ℕ and that we can compute from an index what proposition each proof proves. (Again: not actually countable in DL but that isn't important for the moment.)

Notationally, let's say:

  Proofk ∈ ℕ
    the family of proofs in the subject system

And define a relation between two natural numbers, k and n:

  k iProves_self_applied_iForm n <=>
    the proof Proofk is a proof of Iformn(n) 

Leading up to his "first theorem" Goedel spends quite a few pages getting to this point. I hope this time I've said it better than I said it last time, and that this abbreviated version is familiar territory.

Here is something really subtle about Goedel numbering, but very, very important.

Goedel's first theorem assumes proofs can be enumerated, and formulas with a free variable can be enumerated.

Most importantly... this is the key point of Goedel numbering ...

To establish a contradiction, Goedel's theorem 1 assumes that the relation k iProves_self_applied_iForm n is decidable by a some procedure that takes a numbers k and n as input, and then outputs either True or False.

Even though a procedure that computes k iProves_self_applied_iform n is working only with integer k and n, we know (metamathematically!) that if it returns True, that the k^th proof proves the nth sentence iForm_n(n).

Since "iProves_self_applied_iForm" is assumed to be a computable relation between integers, Goedel assumes it can not only be defined metamathematically, but also in the target system. In the target system it is not defined in terms of forumulas and proofs. It is just a defined relation between any two natural numbers.

Here is Goedel's first use of a fixed point, in the first theorem.

He metamathematically defines ParadoxFormula to be a family of formulas in the target system, using this recursive definition:

ParadoxForumalai := IFormi(i)
                   where Iformi is a subject system 
                     formula, with free variable x:
                     "~(x ∈ { j ∈ ℕ | ∃ k ∈ ℕ s.t. k iProves_self_applied_iForm j })"

We have here metamathematically defined a family ParadoxFormula, indexed by a (so far unclear) subset of ℕ.

If the family ParadoxFormua_i is not empty, then let:

  q := the least index of ParadoxFormulai
  Paradoxical = ParadoxFormulaq

In other words, we have (metamathematically) define Paradoxical to be a least fixed point of the open formula ParadoxicalFormua.

Paradoxical is a sentence in the subject system, metamathematically defined as a fixed point.

Completing the proof of Goedel's first incompleteness theorem should be easy from here.

If Direct Logic is the target system, the definition of Paradoxical violates the rules of construction for sentences.

Goedel's handwave of a proof of his 2nd (so-called) theorem begins -- I claim this is a fair paraphrase --

Copy the afforementioned definition of the sentence Paradoxical but delete every mention of "metamathematically". Treat all of that as definitions in the subject system itself. Then.....

ParadoxForumalai := IFormi(i)
                   where
                   i is the index of a subject system formula,
                     "~(i ∈ { k ∈ ℕ | k iProves_self_applied_iForm i }"

First, I think the formula you were going for was "~ exist k ∈ ℕ s.t. k iProves_self_applied_iForm i." (If not, that doesn't affect the rest of what I'm saying. In fact I'll continue using your version in this post just in case.)

Second, you're using three variables i here. I can't tell if IForm_i(i) is supposed to be taking i from the subscript parameter or from the local binding in the "where" clause. How about cutting to the chase:

i := the index of a subject formula with free variable n,
    "~(n ∈ { k ∈ ℕ | k iProves_self_applied_iForm n }"

Paradoxical := IFormi(i)

If Direct Logic is the target system, the definition of Paradoxical violates the rules of construction for sentences.

Why does it violate the rules of construction? The sentence Paradoxical is structurally of the form "~(i ∈ { k ∈ ℕ | k iProves_self_applied_iForm i }," with i and iProves_self_applied_iForm replaced with their elaborate number-theoretic definitions. Since Classical Direct Logic embeds full second-order Peano/Dedekind axioms for ℕ, it should be able to express everything in the sentence.

Ross, thanks for pointing out a bug in the definition I gave for Paradoxicali. I fixed it above and will unpack it here. The (hopefully) fixed version is:

ParadoxForumalai:= IFormi(i)
                   where Iformi is a subject system 
                     formula, with free variable x:
                     "~(x ∈ { j ∈ ℕ | ∃ k ∈ ℕ s.t. k iProves_self_applied_iForm j }"

Recall that Iform_{i ∈ ℕ} is assumed to be a family of all subject system formulas with one free variable.

As an intermediate step, we could define a sub-family:

PotentialParadoxicali = IFormi
                   where Iformi is a subject system 
                     formula, with free variable x:
                     "~(x ∈ { j ∈ ℕ | ∃ k ∈ ℕ s.t. k iProves_self_applied_iForm j }"

The family Paradoxical_i is an image of PotentialParadoxical_i by the operation of self-application-of-index:

  Paradoxicali := PotentialParadoxicali(i)
                             for all i that are index of 
                             PotentialParadoxical

If the family Paradoxical_i is not empty then pick any member (such as the least) and you have a sentence which, if it can be proved, the proof's index serves as a counter-example and yields a contradiction.

We defined Paradox to be a member of the family and, for convenience, the least member.

Paradox := Paradoxicali where i is the least index of Paradoxical

It's really critical to Goedel that the families of formula, sentences, and proofs we're talking about here be effectively enumerable. For example, the formula IForm_i can be interpreted as a function:

   Iform : ℕ ↦ formula of one free variable

   Iform[i ∈ ℕ] :  ℕ ↦ sentences

   Paradoxical : a particular domain restriction of Iform

   Paradoxical[i ∈ ℕ] : a particular domain restriction of Iform[i ∈  ℕ] 

It is also critical to Goedel's argument that each of those functions not only be computable, but that it's inverse must also be computable.

The definition of Paradox is (for Goedel's argument purposes):

  Paradox := leastfix λ s . Paradoxical[Paradoxical←(s)]

No matter how you formalize it or how many layer of indirection in the definitions, Goedel's argument requires that the definition of the sentence Paradoxical explicitly expresses one of the (integer) terms of the definition is the "encoding" of Paradoxical.

Sentences in DL are defined by categorical induction, a kind of construction method. J. H. Conway has a handy metaphor for this kind of construction in terms of a numbering of days.

On Day 0, some specific sentences exist.

On Day 1, new sentences can be created from those from Day 0, none of which are equal to any Day 0 sentence.

On Day 2, new sentences can be created from earlier made sentences, none equal to any earlier made sentence.

etc.

Sentences in Directly Logic can not be computed by arbitrary computable functions. None of the functions that can construct a sentence in Direct Logic have any fixed points.

The (hopefully) fixed version is

Minor nitpicks: The parentheses are unbalanced. You're also using "x ∈ { j ∈ ℕ | ...(j)... }" where you might be able to say "...(x)..." directly. Later on, what do you mean by "categorical induction" as a construction method? When I look it up, it's a philosophy of science concept and I don't see the connection.

Major nitpick: I still think your ParadoxFormula_i "family" doesn't use i for anything; it defines its own i inside rather than actually depending on the index. Or are you allowing that there may be more than one index i corresponding to the same formula?

If you are allowing that, how do you reconcile that with saying that Iform's "inverse must also be computable"? If you're not allowing that, then you've already constructed a single sentence, and I see no reason for you to define:

  Paradox := leastfix λ s . Paradoxical[Paradoxical←(s)]

---

No matter how you formalize it or how many layer of indirection in the definitions, Goedel's argument requires that the definition of the sentence Paradoxical explicitly expresses one of the (integer) terms of the definition is the "encoding" of Paradoxical.

At least we're on the same page there.

Sentences in Directly Logic can not be computed by arbitrary computable functions.

I'm very unclear on how Sentences in Direct Logic work. The rules you pointed me to on page 27 are just introduction rules, with no elimination rules, so there's not much point in defining any functions that take Sentences as arguments.

Even the introduction rules seem a bit incomplete. They refer to free variable information, but this information doesn't seem to be tracked in the types, so I'm not sure how it's extracted. Meanwhile, it seems like there's no way to construct an (x:Variable◅aType▻) without first building an expression that binds it, and I'm not sure how (and whether) that circularity is well-founded.

There's at least some way to construct (a certain subset of) Sentences from strings. If that subset is strong enough to describe arbitrary computable functions, and if the string-to-sentence coercion is one of those computable functions, then we can probably write quine strings that describe themselves. Then we get to ask if these self-describing strings are strong enough to cause problems.

Personally, I suspect it's possible to make the self-describing strings but not possible to combine them with the self-proof of consistency. Hewitt claims it's not even possible to use sentences to make fixpoints, but I don't see enough details about the string-to-sentence coercion to know that for sure.

A string must type check in order to be parsed into a sentence of Mathematics.

String for Y combinator fixed point does not type check.

Also, in Direct Logic there is no such thing as a "formula."

This responds only the "major nitpick":

I still think your ParadoxFormulai "family" doesn't use i for anything; it defines its own i inside rather than actually depending on the index. Or are you allowing that there may be more than one index i corresponding to the same formula?

Same up to alpha-renaming, yes. This would be true in the case of Goedel's specific construction.

Notationally:

  IFormi ∈ ℕ :=  "some formula with x free"

defines a family indexed by the naturals in terms of a typical member, Iform_i.

Here is a formula with x free:

  ~(x ∈ { j ∈ ℕ | ∃ k ∈ ℕ s.t. k iProves_self_applied_iForm j })

There is a subfamily of Iform_i which are equal to that formula, up to alpha-renaming.

That subfamily could be defined this way, again in terms of a typical member:

PotentialParadoxicali := IFormi
                   where Iformi is a subject system 
                     formula up to alpha renaming,
                     with free variable x:
                     "~(x ∈ { j ∈ ℕ | ∃ k ∈ ℕ s.t. k iProves_self_applied_iForm j }"

Note that the index set of the family PotentialParadoxical_i is a subset of ℕ

The index set of the family Paradoxical_i is the same as the index set of PotentialParadoxical_i.

The family Paradoxical_i defined in terms of a typical member is:

  Paradoxicali := PotentialParadoxicali(i)

                          == Iformi(i)
                             for all i in the index set of 
                             PotentialParadoxical

                          == a sentence of the form
                             ""~(i ∈ { j ∈ ℕ | ∃ k ∈ ℕ s.t. k iProves_self_applied_iForm j }"
                             where i is the index of 
                             this member of the family

                          == Iformi(Paradoxical←Paradoxicali)

Same up to alpha-renaming, yes.

Ah, okay, that answers the questions I asked.

Why do you then build up to this, though?

Paradoxicali ==
  Iformi(Paradoxical←Paradoxicali

If you think you need fixed point definitions to make that observation (not definition), then the same would apply to any other invertible function. For instance:

Identityi := i

      == Identity←Identityi

Why do you then build up to this, though?

  Paradoxicali := Iformi(Paradoxical←Paradoxicali)

Just to emphasize that Paradoxical_i is a specific family of fixed points.

(You can abstract the mention of Paradoxical_i from the right hand side and install a fixpoint operator instead.)

In Hewitt's system, this definition:

X := q ∈ K where (X == Rq(q))

is ruled out.

That's still too informal to me. (Though I am clueless what that proof is about.)

The thing which bugs me: For Presburger arithmetic I have a proof that it is consistent and complete. If I expand it with multiplication, I arrive at the logic of Godel, multiplication is one of the the constructs Godel relies upon, and I have a proof the system becomes consistent and incomplete.

But Hewitt hasn't presented a formal definition of his language. He claims it doesn't allow fixed points but he hasn't proven it. Then now this argument which claims that a construct is ruled out in since it relies on the definition of a fixed point which cannot exist in his formal system which doesn't exist.

Hewitt needs to state a formal system. A language description with type inference rules, a proof that fixed points cannot be expressed, and a proof that the construction above cannot be expressed within his system.

It's all daydreaming.

The Church/Turing inferential incompleteness theorem is not about arithmetic.

Gödel numbers are a "red herring" when it comes to inferential incompleteness ;-)

There is a formal definition of Classical Direct Logic here: Inconsistency Robustness in Foundations

Comments and suggestions for improvement are greatly appreciated.

Thomas,

You are correct: the Direct Logic proof of the consistency of Mathematics (by itself) is not dispositive because Direct Logic could still be shown to be inconsistent.

Cheers,
Carl

Does this mean the proof of consistency of mathematics is contingent on Direct Logic not being part of mathematics? Yet it seems distinctly mathematical?

Does this mean the proof of consistency of mathematics is contingent on Direct Logic not being part of mathematics?

Classical Direct Logic is, for convenience, called "Mathematics".

Classical Directly Logic ("Mathematics") is proposed as a foundations of mathematics for Computer Science.

To answer your question: Classical Direct Logic is within mathematics. It is proposed as a foundational theory for mathematics.

How can that be true if Direct Logic can prove the consistency of mathematics, but it itself may still be proved inconsistent? Doesn't that require that direct logic is not part of mathematics, otherwise we already have proof of its consistency?

Classical Direct Logic tells us that it's consistent, but that's what an inconsistent system would say. :)

In that way, a self-proof of consistency has pretty limited value.

Still, it's almost comical how we justify the use of mathematics. If anyone doubts a system's consistency, we retreat into a stronger system to argue for its consistency. A self-proof of consistency would let us at least keep talking about the same system.

I don't know what cultural effect this would have. This stability might let us be even more stubborn, or it might let us stand still long enough to learn something.

To be more specific (and setting aside Gödel for a moment), a self-proof of consistency has in itself exactly no value. Because you will have motive to believe it exactly when you already believe the self-proving system to be consistent. A proof of consistency based on a subsystem of the system, which Hilbert had been hoping for, would have the benefit that you'd know if the subsystem is consistent then the whole system is consistent. A proof of consistency based on a supersystem of the system may be informally interesting if it increases understanding of the relationships between different principles of deduction, different axioms. A self-proof of consistency by a system that's designed to not explode if it turns out not to be consistent? That has mildly negative value, because clearly the system itself is designed on the expectation the self-"proof" might be wrong. But of course when you stop setting aside Gödel, you lose the proof-by-subsystem and self-proof options, because when those happen (for a system that isn't underpowered) you know it's not conistent. So the proof-by-supersystem is the only one of them that does't disprove consistency anyway.

The Mathematical self-proof of consistency shows that convincing proofs may be possible.

The Mathematical self-proof of consistency shows that the current common understanding (based on Gödel's writings) is inaccurate.

Although Mathematics can prove its own consistency, it may turn out not to be consistent.

How can that be true if Direct Logic can prove the consistency of mathematics, but it itself may still be proved inconsistent?

A consistent theory can contain a proof of self-consistency.

An inconsistent theory can also contain a proof of self-consistency.

DL is one of those two cases but it is conservative enough that betting it is consistent is probably a good bet.

Doesn't that require that direct logic is not part of mathematics,

Now I'm not sure at all what you mean by "part of mathematics".

The Church/Turing proof of inferential incompleteness has no fixed points; but Gödel's "proofs" depend crucially on the existence of fixed points.

Thomas,

You are correct:

"contra Gödel" is that Gödel was able to get away defining sentences
by fixed point that way only because of a confusion at the time. That,
indeed, the syntactic restriction Hewitt proposes should be universal
to all of math. Permitting self-referential sentences in any but a
trivial system is, after all, a way to instantly make the system
inconsistent!

Cheers,
Carl

How would I write Zeno's paradox in Direct Logic, and calculate its fixed point. I would like to see the code.

Goedel's method requires the target system to permit a sentence to be defined as a fixed point of a formula containing S itself.

Keep in mind Gödel's target system is just first-order Peano. Maybe all you mean is that fixpoints are admissible, but that's a pretty surprising theorem (Löb's theorem), not something the system goes out of its way to "permit."

If we had a readable enough Gödel sentence to look at, it wouldn't have a special syntax for saying "this sentence." Instead, it might look like a quine.

Hewitt is (at least claiming, plausibly) to point out that Goedel did not kill Hilbert's program at all. In fact, Hewitt has a candidate system to do what Hilbert wanted.

Going by W. W. Tait's "Gödel on Intuition and on Hilbert's finitism," it looks like Gödel himself made sure to point that out in the incompleteness paper, and he kept on thinking about finitary foundations long after that.

---

Since you like the idea of a foundation that can self-prove its own consistency, I recently found another one you might like. (I hope Matt M is reading too.)

Andrew Boucher's "Arithmetic Without the Successor Axiom" describes a weak arithmetic called F. As far as I can tell, the reasoning in this paper isn't peer-reviewed, but it's at least chock full of (IMO) readable proofs, and it talks realistically about prior work and room for future improvement.

F arithmetic has full-powered second-order induction, but what makes it unable to invoke first-order Peano is that it can't prove the existence of any number's successor. It proves its own consistency in the sense of showing that no proof of "0 doesn't equal 0" exists. It does that by showing that its axioms and inference rules all preserve a predicate that amounts to "true in the trivial model where the only number that actually exists is zero," which that sentence doesn't satisfy.

If we trust a traditional foundation like ZFC, F is clearly consistent by that argument.

If we distrust ZFC and take F as a foundation, then our proofs may themselves be too large to exist, including the self-consistency proof. Fortunately, that document claims something reassuring: If any proof of "0 doesn't equal 0" exists, then that proof must be large enough that the consistency proof exists first! I don't really follow the proof of that claim, but it's fascinating to think that perhaps all our core requirements for a mathematical foundation can be satisfied in a system with not only a finite symbolic specification, but a satisfactory finite model, which then lets us talk about an alternative, infinite model from solid ground.

At this point, I think Andrew Boucher's F arithmetic (or one of its variations and consistent extensions described in the same document) could be a very promising addition to the superstitious total compilers Matt M was describing a couple of years ago. Both ideas seem to be revolve around the exact same kind of agnosticism toward large numbers.

F arithmetic seems interesting. Here's a long thread from the n-category cafe discussing various weak models of arithmetic, including F.

Keep in mind Gödel's target system is just first-order Peano.

Not in the second theorem.

If we trust a traditional foundation like ZFC

I'm not sure if Hewitt's would need "C".

I would if you could augment F with an axiom that would let you establish the existence of any particular finite Natual without letting you generalize, as I described in that thread. And if you did so, I wonder if it would still be complete.

(I'm hard at work right now, so trying to limit LtU time.)

If you assume the existence of any number, F supposedly lets you show the existence of all smaller numbers down to zero, but not the bigger numbers. I think that's what you want, right?

And if you did so, I wonder if it would still be complete.

It's not complete. It has multiple models.

No I want the ability to prove the existence of any finite number but not to prove the existence of every number - meaning with a quantifier.

Well, nope, this system doesn't let you just prove the existence of any given finite number. Adding that capability would probably destroy the self-consistency proof the way it's written, since the axioms would no longer be true for the zero-only model.

Hmm, there might be another way to state the self-consistency proof so that it shows that in a model of a given size (no smaller than the proof of this very self-consistency theorem), all the proofs that can be encoded in that model are consistent. I assume we'd add an axiom schema that would establish the existence of any given finite number, as long as we fully write it out. That way the axiom instance itself will be too large to exist unless the number it's talking about also exists.

Someone would have to actually prove it in that form, of course. Unfortunately, I'm not confident in the validity of Boucher's original proof, so I'm not confident this alternative theorem can be proven either. (Right now, my biggest doubts are seeded in the worry that we'd need to take every possible proof encoding scheme into account... and perhaps there are schemes where self-consistency proofs are artificially larger than proofs of "0 doesn't equal 0.")

Thomas,

You have it almost exactly right!

Mathematics (formalized using ⊢) is its own meta system and can be used to formalize at theory T (using ⊢_T) even is T is inconsistent.

Of course, Mathematics must be both consistent and very powerful.

Cheers,
Carl

It turns out from a pure functional programming perspective, instantiating an object is an application of the fixed point operator. See the OOHaskell paper: http://arxiv.org/pdf/cs/0509027.pdf

Mathematics is founded on the categorical induction axiom:

∀[P:Booleanℕ]→  Inductive[P]⇨ ∀[i:ℕ]→ P[i] 
  where  ∀[P:Booleanℕ]→ Inductive[P] ⇔ (P[0] ∧ ∀[i:ℕ]→ P[i]⇨P[i+1])

From the above axiom, sets over ℕ (said to be the "language of ordinary mathematics") can be constructed using types.

See page 28 of Inconsistency Robustness in Foundations.

Thanks!

Carl

1. a = b   by inspection?!???!!?
Note: step 1 raises a tricky problem.

This is the problem with parameterizing propositions with values. Propositions need to be finite so that you can inspect them. The standard way that everyone does this, with propositions and proofs as finite pieces of data that can be inspected in their entirety, seems like the right way to go. I don't see any advantage to what Hewitt is doing here. The only way that we'll be able to prove things about arbitrary values is if 1) the implementation somehow gets a handle on their generating expression or 2) we can make due with finite inspection (in which case a finite expression can capture the relevant information). So why not just reason about expressions like everyone else does?

And if they are equal but no proof can ever show it [...]

Where did the assumption that 'no proof can ever show it' come from? In my (hypothetical) model there is a proof for every true proposition. If they are equal, then there is a proof they are equal.

Why parameterize propositions with values?

In the real world, we can build propositions that way.

Having a powerful system like Direct Logic is important in computer science because computers must be able to formalize all logical inferences (including inferences about their own inference processes) without requiring recourse to human intervention.

To me, the opposite idea -- that every sentence must be (finitely) printable -- seems an odd restriction that limits the directness with which mathematics can model existing reality.

. The only way that we'll be able to prove things about arbitrary values is if 1) the implementation somehow gets a handle on their generating expression or 2) we can make due with finite inspection (in which case a finite expression can capture the relevant information). So why not just reason about expressions like everyone else does?

Option (1) is a real thing that happens in the world.

What is so different between your ability to distinguish written glyphs 2 and 3 versus a computer programs ability to recognize the coincidental structural equality of two Actors about whose values from some message it wants to prove a theorem?

DL abstracts away a lot of stuff to find a common structure.

Where did the assumption that 'no proof can ever show it' come from? In my (hypothetical) model there is a proof for every true proposition. If they are equal, then there is a proof they are equal

If your Oracle can compare infinite lists from arbitrary computations instantly, you've given us enough to derive inconsistencies. We can start counting uncountable things. There would be no consistent truth for your Oracle to report.

To me, the opposite idea -- that every sentence must be (finitely) printable -- seems an odd restriction that limits the directness with which mathematics can model existing reality.

That seems like a superficial idea to me. If you dig into it, what can you even do with such sentences that contain values? If I give you a sentence S = "# = #" and the # are actors that you have to probe to find out what they are... what can you even do with such an object? The whole idea of equality is learning that two different expressions have the same value. Reasoning directly about the values doesn't even make sense to me. The expressions are at the core of what reasoning is.

What is so different between your ability to distinguish written glyphs 2 and 3 versus a computer programs ability to recognize the coincidental structural equality of two Actors about whose values from some message it wants to prove a theorem?

I think it's a fundamental aspect of symbols that they be readable in (tiny) finite time.

If your Oracle can compare infinite lists from arbitrary computations instantly, you've given us enough to derive inconsistencies.

I don't think so, because there's no way to incorporate the turnstile into a computation. The interpretation of turnstile as an oracle happens in the model. It's not available to the language as a computational element.

Again, DL comes from a perspective that contemplates math as a social and as a computation process.

In 1927, if I wanted to hand you an alleged proof I had worked up, I would write it on a piece of paper. The real number constants in my proof would have to be expressible using a finite number of digits, or as the definition of some constractable real (e.g. π).

To assess my proof, to verify it, you would have to make sure the logical structure of it was right, and you would also have to verify certain things by inspection.

If I wrote "1 = 1" for example, you'd have to settle whether I got that right or not by inspection.

Today, at least in thought experiment, I am not limited to writing on paper. I could show you my proof in the form of an interactive hypertext.

A real number could be displayed as a button that reveals successive digits, each time you click it. (How it obtains the digit is not germane, other than it could be by non-deterministic choice.)

If two such real number are joined by an equals sign the equals sign could itself be a button. If you click on it, either it will (correctly) tell you the two reals on either side are equal, considering infinitely many digits in their expansion. Or it will tell you (correctly) they are not equal. Or it might just hang.... The key thing is: you can assume it will never give a wrong answer.

Notice that we have abstracted away any concern of how equality of constants is judged when verifying a proof. This is nothing new. We abstracted away that same judgement when proofs were confined to paper. Someone might say: "Looking at squiggles shaped '1 != 2' how do you know the squiggle '1' is different from the squiggle '2'?" A mathematician would say: "What, are you crazy? Just look at it." Since we can automate "just look at it" in interesting ways, we can allow in constants that aren't classically constructable.

A foundation for mathematics, especially one for computer science, should not exclude that second kind of proof that is at the same time on one hand a finite hypertext, and on the other hand contains infinite lists of digits.

That's an example of why (in my opinion) it is a good idea that DL makes a very conscious distinction between abstract sentences, a kind of syntax tree, and strings, the kinds of things you can write on paper.

Where's the proof in your example? This equals sign button you've described sounds like a semi-decision procedure. If the implementation is particularly transparent, it would be a sensible way to define equality of reals. Otherwise, if equality of reals has some other independent definition, we'd have to reason about the implementation to prove that it's a correct procedure. Granting one of these possibilities for now, I would then only agree that you've proven two real numbers equal if you've pressed the button, and it came back with the answer "yes, they're equal". If you tell me you've got a proof, it's running now, it may never stop ... well, that's not a proof.

Otherwise, we have a proof of Goldbach's conjecture, as we're in the same situation with it: we've got a semi-decision procedure which will, in this case, never return "true", but will either return "false" at the first counterexample, or simply hang. (According to Wikipedia, there's no counterexample below at least 4 * 10^18). It should be obvious that any actual proof of Goldbach's conjecture needs to consist of a finite piece of reasoning, conclusively showing that the semi-decision procedure will never stop with a "false" answer.

I'll also point out that situations like your example are routinely modeled in computer proof assistants all the time; there's no sense in which they've been "ruled out". Unless you mean we've ruled out infinite proofs, which I maintain is a good thing.

Where's the proof in your example? This equals sign button you've described sounds like a semi-decision procedure. If the implementation is particularly transparent, it would be a sensible way to define equality of reals.

It might be helpful to remember that mathematics is something that people (and machines) do. It's an activity. So, how does that help?

Suppose I give you a proof like this:

Theorem: 1 = 1
Proof:
    1 = 1     by definition of = and inspection
    QED

It looks right, right? The definition of "=" says that every number is equal to itself. And you can plainly see that in "1 = 1", the same number occurs on both sides of the equal sign.

Wait: Where's the actual proof that the number "1" is really on both sides of the equal sign? Answer: it's external to the formal math itself. It's in your head. It's a social fact. It's an empirical fact. Outside of the formal math, we can all stand around and look at the piece of paper, and agree: "Yup, that's a digit "1" on both sides of the equals sign, denoting the equality of the number 1 to itself."

When I show you the hypertext document with an equals sign button you can push to (maybe) get a judgement about two constants, it's similar. I'll be happy to take you back stage and show how the button is wired. How it works. I'll offer engineering arguments for why would should believe it only gives correct results, giving no result if it can't judge equality. We can all stand around and scrutinize the machine the runs the "=" button. But all that activity is outside of the formal math.

Traditional math is a way to reason about outside-of-math judgements like the equivalence of symbols on paper (which math abstracts as equality of numbers).

Why are we restricting ourselves to paper and refusing machines that can augment our ability to judge equivalences of representations?

You didn't answer my question, I think because I failed to ask it clearly. In the example with the equals button, what exactly is supposed to count as a proof of something? I'm happy to entertain your scenario, and I'm the last person who would argue for restricting ourselves to paper. I just don't see what the scenario has to do with proving anything.

In the example with the equals button, what exactly is supposed to count as a proof of something?

You already know the answer. A proof is correct if it is a series of propositions, each of which is either axiomatically true, or true by an allowed form of deduction from the earlier propositions.

The example of the "equals button" concerns the question of how we check to see if a step in a proof has been done correctly. In my trivial example proof, is the step that asserts "1 = 1" correct? That judgement needs to be made, outside of the formal system, to see if my proof is right.

There is a world-historic shift in the practice of mathematics in which machines are playing a new role in making the judgements we associated with verifying proofs. It has lots of interesting consequences, such as sharpening the distinctions between that which is provable, that which is true, and that which is (merely) consistent.

Thanks for your reply. My understanding now is that you intend the equals button example to be admissible in a proof as a single step, analogous to the 1=1 example, albeit one whose verification may hang. If so, then I think I can claim to have a proof of Goldbach's conjecture in such a system, since that conjecture is equivalent to the statement that a certain real number is zero. (Take the nth binary digit to be zero iff n is the sum of two primes.) Apparently, I can just claim this equality as a single proof step, verifiable by inspection, perhaps with a button. Of course verification would hang. Maybe you can appreciate why I might find this terminology shift problematic? I was merely suggesting that we insist verification actually complete before granting the label "proof". My follow up argument is that as soon as we do so, we effectively make proof data finite, assuming verification is practical and not an oracle for example.

Mathematics is historically a social activity and increasingly an activity of societies of people and networks of machines.

"Nodes", like mathematicians or servers, can transmit impossible-to-substantiate or even wrong proof-claims to other nodes, and yet somehow mathematics lumbers on. A mistaken claim invalidates work that assumed it was true and leaves other work unscathed. So long as no inconsistency is discovered in a foundation, it too remains unscathed.

An "equals button" would certainly have to be empirically convincing to be credible. How convincing your claim of a proof is would hang on the details of your machine.

In the specific case of the Goldbach conjecture, it's implausible that we need to produce any unconstructable real constants or other infinite-information constants to carry out a proof. Any eventual proof, if there ever is one, would probably be of the kind that can be fully expressed in finite strings that you might write down on paper.

I can understand the idea as a call for generalization: classical propositions allow literals, so let's allow arbitrary literals in our propositions. But I see it as fundamental to literals, as parts of expressions, that they be finitely recognizable. Look at a simple example of what formal reasoning looks like:

    |- a = b     |- b = c
------------------------------
           |- a = c

Trying to make sense of a schema like that when you can't finitely recognize the entities under discussion doesn't make sense:

    |- # = #     |- # = #
------------------------------
           |- # = #

Note that if these are literals and these equations actually hold, then all of the hashes are the same literal. This doesn't seem to be the same thing that's happening with reasoning inside a formal system.

Also, responding to your point about knowing that '1' is different from '2' by inspection -- that's not actually how many logics work. For example, in Peano Arithmetic, '1' and '2' are aliases for 's z' and 's s z'. That they are not the same is a theorem.

I can see the utility in introducing literals naming computational entities from some environment. But, again, I think the right mechanism for this is one of finitely recognizable names. Otherwise it doesn't seem to fit in with what propositions are.

Trying to make sense of a schema like that when you can't finitely recognize the entities under discussion doesn't make sense

Yes, of course. That's right. That's why Hewitt describes Proof? as total computable. All judgements in a proof must be performed in finite time, etc. (Proof? can hang on non-proofs, by the way.)

The issue here is the information content of allowable constants.

If we allow only Sentences which can be parsed from finite Strings, then all the constants in our Sentences have only finite information.

Yet using media other than paper we can manifest constants containing unbounded information. Since these kinds of constants contain unbounded information, they can't be expressed as a finite String.

The first schema you gave is just fine:

    |- a = b     |- b = c
------------------------------
           |- a = c

We can, using computer programs for example, construct material representations of Sentences, to which your schema might be applicable, even though the Sentences in question have no finite representation as a String.

The equivalence of the glyph "2" and the glyph "2" is not found in formal mathematical theories of numbers, yet you need judgements of that equivalence to do any formal math about numbers.

Using machine we aren't limited to manifesting constants using finite sequences of glyphs. We can manifest a constant using circuits and software, for example. We can manifest constants with no finite representation as a string. In some cases, we can make true judgements about the equality of these kinds of constants.

Actually, as long as the actors are generating expressions, I don't see why you couldn't include them, in principle.

For example, rather than thinking of it as embedding a literal 3.1415926... into a sentence text, we could think of it as embedding an expression generated by an algorithm that expands to (3 plus-tenth (1 plus-tenth (4 ...))). I can imagine a framework for reasoning that such an infinite expression is equal to some other definition of pi, such as a series sum.

I'm still having a hard time imagining why this would be useful. What benefit comes with this complexity? (What complexity? You have to explain limits in order to evaluate expressions). I can reason about pi just fine with the usual approach of finite expressions without all of the headaches.

To find this compelling, I'll need an example of something useful that this approach makes possible. So far, all of your examples appear to be of things that are easily (and IMO much more naturally) expressed within more standard frameworks.

Actually, as long as the actors are generating expressions, I don't see why you couldn't include them, in principle.

The definition of an Actor is a finite string.

A manifest Actor is a physical entity.

A single Actor definition can produce an uncountably distinct number of manifestations.

In Actor programming languages, that situation can be described with operations for non-deterministic computation and delayed (lazy) computation.

I think part of your mental block here is that you are confining your interest in "mathematics" to (more or less) theorems of the sort that could be usefully written down in a text book and spread around the world and read years later. Not all useful theorems have to be communicable that way. We can have useful theorems about things for which you "had to be there".

What benefit comes with this complexity? (What complexity? You have to explain limits in order to evaluate expressions). I can reason about pi just fine with the usual approach of finite expressions without all of the headaches.

All of your arguments about pi can presumably be transcribed into a DL-founded theory quite directly. You aren't losing anything.

To find this compelling, ...

"What can we do with this?" is indeed an interesting question. A lot, I think, but it's a big topic.

I'm unconvinced, but we'll see.

Inferring that x=y in Mathematics requires an actual proof ;-)

A single Actor definition can produce an uncountably distinct number of manifestations.

As I understand it:

• We start with a finite actor system (finite actors, finite messages)
• In each step, an actors system processes one available message and adds a finite number of available messages.
• For any finite number of steps, our actors system has a countable number of possible configurations.
• If I ask for an infinite number of steps, the resulting actors system will never physically manifest.

It isn't clear to me how you'll ever reach the 'uncountably infinite distinct manifestations'.

While this likely won't help, there's a book about metaphors which specifically addresses the issue of deriving the idea of infinity from repeating a process indefinitely. Also, the authors were not computer scientists, which prevents a "breathing our own exhaust" quality that might otherwise obtain.

When it was new, I read Where Mathematics Comes From by Lakoff and Nunez, because the general theme matched a naive intuition I had formed about how folks perceive mathematical entities as "real" by virtue of fitting nicely with human cognition (it feels good).

The discussion of infinity is pretty interesting. If you ask a normal human being to try to distinguish between reasoning about what happens "if we keep doing this indefinitely" and reasoning about the reified infinite result of having done that (despite the fact we can't), they're going to have trouble. I'd expect conversation to bog down.

If mathematicians have a jargon that resolves that by magic incantation, how do we distinguish that from mere rules in a game? I only ask that to suggest sometimes folks deny a game or rules are involved in the infrastructure of terms used in discussion.

Actors can be non-deterministic. It's a fairly early page in the paper. There's a sentence at the top of the page that starts something like "there are uncountably many actors". There's a one-line program there of some interest to this thread.

Non-determinism was already accounted for above. Each step processes one message from a finite set of available messages. Which message is not deterministic. But this still only gives us a finite branching factor based on the set of available messages.

Hewitt seems to be arguing for infinite actor systems, e.g. with arbitrary real numbered values or actors of infinite size or infinities of actors. With that assumption you could probably reach some uncountable infinities, but you'd certainly be unable to manifest any infinite system (i.e. by your earlier description that "a manifest actor is a physical entity").

By a diagonal argument, there are uncountably many Actors.

See page 10 of Inconsistency Robustness in Foundations

Consider the Actor definition (from the paper):

  Real.[] ≡ [(0 either 1), ⍒ Postpone Real . []]

The value denoted by the definiton of the nullary message is an infinitely long list of bits, each chosen randomly and independently of the others. The constant denoted contains an infinite amount of information.

That denotation accurately describes how programs can use such a value and how the value can be treated in mathematical propositions and proofs.

Of course, in an implementation bits are produced only on-demand so at no point is infinite storage needed.

Does a recipe for a cake 'denote' a cake?

I'm not sure how this actor definition denotes anything other than an actor definition. If you instantiate it, you'll have an actor system. Everything I noted above still applies. The amount of information involved is finite.

Note that I specifically quoted your sentence where you said we'll have uncountably distinct manifestations, where you described 'manifest' to mean the physical sense. In that context, pointing out what a generating process for an infinite string of bits/cakes/etc. might 'represent' to a mathematician in some non-physical universe doesn't seem very relevant.

An Actor can evolve into any of uncountably many different Actors.

Edit: I.e., an Actor can evolve into a real number that is different from any element in a countable set of real numbers.

Given infinite time.

My ex does this too.

if you have reals (infinite memory) and the time to distinguish reals (infinite time).

If an actor is defined as having a program of finite length and state of finite length it can only have a countable number of states.

If you claim otherwise then you don't understand what "countable" means.

Also the number of actors with finite addresses is countable, therefore any uncountable set of actors is a set that requires infinitely long addresses.

Also, being able to represent a number that isn't rational has nothing to do with being able to represent the whole set of reals. The set of numbers you can represent in a 1 to one correspondence with a finite program and finite state is countable.

On another topic if you're considering every possible computer program as completed no matter being infinite, then you're into a superset of anything that mathematics has ever taken to a limit. This isn't guaranteed to be analyzable, and certainly full of paradoxes.

pointing out what a generating process for an infinite string of bits/cakes/etc. might 'represent' to a mathematician in some non-physical universe doesn't seem very relevant.

Unless, say, a programmer wants to reason mathematically about the behavior of his programs, or a mathematician wants to have some physical intuition for his inductions. Other than that, it's just words on paper possibly.

It might theoretically be relevant in a completely different context than the one specifically regarding "uncountable distinct number of (physical) manifestations" for actors.

Though, it seems easier to reason mathematically about the co-inductive generating process. No need to involve infinities. Even mathematicians have a difficult time reasoning about real numbers. A lot of reasoning about infinities simply doesn't apply to computation, e.g. Ramanujan sums (1 + 2 + 3 + ... = -1/12).

You are eliding the quote you take from me.

I said that a single actor definition can give rise to an uncountably distinct number of (physical) manifestations.

How many different possible physical manifestations can a single actor give rise to? Uncountably many.

This is not even controversial.

Though, it seems easier to reason mathematically about the co-inductive generating process. No need to involve infinities.

A countably infinite number of bits is entailed in the concept of an infinite, lazily evaluated list. Again, this is simply an ordinary literal truth, hardly anything controversial.

A lot of reasoning about infinities simply doesn't apply to computation, e.g. Ramanujan sums

That's very interesting. Which page in the paper are referring to?

For any finite time (e.g. measured in a count of messages processed), the number of possible manifestations for an actor system is finite i.e. with a finite branching in each step. The physical universe will never experience infinite time. Hence a physical actor system does not give rise to uncountably many distinct physical manifestations.

A countably infinite number of bits is entailed in the concept of an infinite, lazily evaluated list.

If you ignore the 'lazily evaluated' aspect, then all you have left to reason about is 'infinite list'. But programs are finite. Lazily evaluated lists have finite encodings. If you don't ignore this aspect, you can leverage it in your mathematical reasoning.

Which page in the paper are referring to?

That was a general observation. Reasoning that requires infinite steps or observations is similar to proof-by-contradiction, relying on a truth we cannot observe.

Hence a physical actor system does not give rise to uncountably many distinct physical manifestations.

Right. Also, the one-line definition shown defines uncountably many physical actor manifestations. (I think you are just having trouble parsing my sentence.)

You've been using the word "physical" in a very confusing way throughout this thread to include non-physical mathematical idealizations. I can only make sense of your claim here if I change "physical manifestation" to "non-physical idealized manifestation," for the reasons dmbarbour has spelled out, quite clearly I think. For another example, you used the absurd phrase elsewhere in this thread that "using media other than paper we can manifest constants containing unbounded information." I have no idea what you could mean there. I think it would help, for clarity purposes, if you distinguished between the actually physical, and mathematical idealizations of physical systems that are based in physical intuitions, but drop certain physical constraints (like finite time).

You've been using the word "physical" in a very confusing way throughout this thread to include non-physical mathematical idealizations.

Consider the cardinality of the set of possible outputs from a program.

The set of outputs from the one-line program that defines an infinite list of random bits is uncountable.

"using media other than paper we can manifest constants containing unbounded information." I have no idea what you could mean there.

On a sheet of paper you an only fit some finite number of digits. Using other hardware, you can create a device that produces an unbounded number of digits.

I think it would help, for clarity purposes, if you distinguished between the actually physical, and mathematical idealizations of physical systems

I have been.

The set of outputs from the one-line program that defines an infinite list of random bits is uncountable.

(Sorry to break into another subthread.)

There is no uncountable set here, because there are no completed outputs of the program. It's a program that cannot terminate; there are only partial outputs. And the number of partial outputs from the program is countable.

For any countable set of reals, there is an Actor for a real number that is not an element of the set, i.e., it differs from each element in the set.

Consequently, the set of Actor reals is uncountable.

To add on to what John is saying here, from a different angle, I'd like to note that, as technical points, the fact that 2^ω is uncountable while the set of all finite prefixes of its elements is countable is uncontroversial. These are essentially the two "sides" of the argument here. The real disagreement is as to what exactly the "set of outputs" denotes. I think it's possible to use language so as to be very clear about which set is being considered, and by so doing, eliminate all disagreements.

The real disagreement is as to what exactly the "set of outputs" denotes. I think it's possible to use language so as to be very clear about which set [finite prefixes after N steps of computation vs. 2^ω] is being considered, and by so doing, eliminate all disagreements.

You are talking about two sets: 2^ω and a set of list prefixes of lazily computed lists.

Here is a different way to look at that: Your two sets are really just two aspects of a single "thing".

Here is how I see it....

Let's recall the actor definition:

  Real.[] ≡ [(0 either 1), ⍒ Postpone Real . []]

We can read that as constructing a set of lists by induction.

Roughly:

  0. is a real number
  if X is previously constructed real number then so are X0 and X1

Separately we could define an equivalence relation:

  For real 0.X:

  0.X = 0.X0
  0.X < 0.X1

We have a simple, inductively defined set of prefixes, right? That's the definition. And second we have an equivalence relation among prefixes, right?

An "equivalence set of prefixes" is a set of prefixes, all equal to one another. 0.X and 0.X0 are both in the same equivalence set of prefixes. Each equivalence set of prefixes is countably infinite.

Now please consider the set of equivalence sets of prefixes. This set of equivalence sets describes the reals (from 0 to 1) and their customary ordering.

At the same time -- and isn't this kind of, i dunno, beautiful or something --.....

The same actor definition that gives us a simple set construction of the reals as equivalence classes of prefxies...

The same definition describes a lazy, non-deterministic computation that can be physically realized to produce as output, successively longer members of one of those equivalence classes.

Isn't that cool?

A machine can decide equality between two physically manifest reals by comparing their bits, or by comparing their actor addresses, or by some combination.

A computer with infinite memory and infinite time is not a computer. What are you on about?

A computer with infinite memory and infinite time is not a computer.

I am pretty sure (there might be mistakes but I'm pretty sure) that if you read back over my comments I don't talk about infinite memory or time. It's subtle. I can see how you got that impression, for sure, but... no, not really. There are some hairs to split. It's not easy to grasp at first look, really.

a physically manifest real is a member of some countable infinity at best, not a real.

The set of square roots of integers is not uncountable, etc.

And to be honest you can't even represent countable infinities in a computer.

Good luck storing something on the order of Graham's number in this universe.

If you didn't give the impression of some deep understanding of Hewitt's gobbltygook I would wonder if you know what "real" means or what "uncountable" means.

Your wording here was careful enough that I can agree with more or less everything in your comment. There are some technical points, for example it looks like you're defining a strict order, not exactly an equivalence relation, and it's not clear from what you've specified how one would show that 0.1000... and 0.01111... are in the same equivalence class, but I don't see any obstacles to filling in the details and making everything rigorous.

Isn't that cool?

I do indeed find it cool to think of real numbers as computations that generate successively more accurate approximations, which is an idea that has a long history in constructive mathematics. Some of these ideas have lead to actual computer implementations, which are easy to learn about by googling "exact real arithmetic." At least one implementation is in a proof assistant and doubles as a rigorous logical development of the real numbers. Now it's down to subjective taste, but I prefer these other approaches, as they are rather careful about treating infinities and dealing with computability. (It also helps that they have clear and complete expositions.)

There is no uncountable set here, because there are no completed outputs of the program.

Also you can't represent the continuum with finite programs. This isn't computer science.

Ok, maybe they want to ignore computability and put hypercomputing on some sort of firm ground (which it may not have yet), and use it as if it were normal mathematics... But doing that as an assumption is invisibly changing the subject. It's like a fallacy based on punning words.

[edit] I guess Hewitt and Thomas don't see actors as a model of computing, they don't see actors as programs. They see actors as something like set theory with messages, where infinite processes are treated as complete. That's kind of mind blowing.

It's not CS, but it's interesting.

But you know, Hewitt thinks that self reference is the root of paradox, but if infinities are the root of paradox then he's in for a nasty surprise, because he's pretended infinities into a mock CS as if that were natural. Who knows what the result will be?

I think I could have worded my comment in a better way so that it wouldn't come across as an attack. My hope was that, by using more precise language, we could move the discussion along. I don't think you disagree with any of dmbarbour's observations about actors limited to finite times (correct me if I'm wrong). Do you object to my characterization of programs running for infinite time or unbounded time as being (quite useful) mathematical idealizations? Another good example of a useful idealization is the infinite tape of a Turing machine. If I got stuck in an argument with someone insisting the infinite tape was a real physical possibility, I wouldn't consider that a productive discussion.

The constant denoted contains an infinite amount of information.

Not in a useful sense. What's there is a perpetually incomplete potential to generate further random bits. That's no more "infinite" than any other nonterminating computation. What we mean when we say "nondeterministic" is that later bits in the sequence don't depend on any information latent in the system before they're generated; so at each point in the unbounded computation, there's only as much information there as has been generated up to that point.

Not in a useful sense.

Confronted with you who denies the existence of a useful sense and Hewitt who demonstrates one, which claim should I believe?

Many excellent and some quite old definitions of the real numbers have an inductive character. Hewitt's is one of them.

You seem to be stuck on the notion that Hewitt's inductive definition of reals is parsimonious: That it both stands alongside classical definitions not motivated by programmable computation per se, and that it also can be interpreted as a straightforward program in an actor language.

It is as if by elaborating a parallel between classical math and computing, you feel Hewitt has taken something away.

Yes, it is odd to talk about a constant with infinite information in the same breath as a physically realizable computation that contains infinite information only in an unbounded future -- yet logically the unification of these two concepts works just fine.

Infinite constants are imaginary. They do not exist. Yes you can talk about them, even prove things about them, but that is simply an existentially quantified statement.

The existentially quantified statement about the imaginary thing exists (because it is finite) and can reasoned about even though the thing it refers to does not exist.

What I don't understand is how to reason about the generator function of a real, if it is an opaque actor. The only way we can prove useful identities on Reals is by algebraic manipulation of the generator function. The only way to get a real number is as the output of a computation anyway. You cannot measure them or input them.

The only way we can prove useful identities on Reals is by algebraic manipulation of the generator function.

Keep in mind that even mundane-seeming proofs of identity are useful in information system. If I say:

x = 3.0
y = 3.0

and ask you to prove that x == y, then after some algebraic manipulation you will have 3.0 ==? 3.0 which you'll solve "by inspection" (such as by a built-in feature of your CPU).

Similarly, if your CPU knows behind the scenes that two bitstreams in question happen to be wired to be copies of a single stream, it can assess their identity "by inspection".

What I don't understand is how to reason about the generator function of a real, if it is an opaque actor.

There is an example.

I am taking about things like the Euler identity, and algebraic manipulation of power series. In the case of 3 == 3 we can prove by structural induction IE s(s(s Z)) == s(s(s Z)).

e comes from natural logarithms, Pi from circles, i as the square root of -1, and yeg they all take part in the Euler identity, along with the trig functions sin and cos.

I don't see how you could prove the Euler identity by inspection.

In the case of 3 == 3 we can prove by structural induction IE s(s(s Z)) == s(s(s Z)).

And yet that itself reduces to showing that s == s and that Z == Z by inspection.

At the bottom of "doing math" either by hand or by machine there are judgements made by immediate apprehension. All I have been saying in this side thread is that immediate apprehension of equality is not limited to comparisons of entities containing only finite amounts of information (as evidenced by the example of a machine that knows two unbounded bitstreams are equal because it has built-in knowledge that they are two copies from a single source).

Confronted with you who denies the existence of a useful sense and Hewitt who demonstrates one, which claim should I believe?

That's not the situation. I explain specifically why it doesn't exist; neither Hewitt nor anyone else can "demonstrate" that it exists, because it doesn't. The definition you provided explicitly specifies a never-ending computation, where the "thing" you claim to talk about is always, throughout the never-ending computation, only partly constructed. Since the computation never ends, the "thing" is always incomplete. You defined it that way; I'm just pointing out what you did.

Why aren't you applying your criticisms to other inductive definitions of ℕ or ℝ?

The definition you provided explicitly specifies a never-ending computation, where the "thing" you claim to talk about is always, throughout the never-ending computation, only partly constructed.

Additionally, interestingly enough, under some circumstances a program can know that two that two such infinite lists of bits are in fact equal.

Why aren't you applying your criticisms to other inductive definitions of ℕ or ℝ?

We weren't discussing those. I was pointing out that you've defined a recursive nondeterministic procedure for generating an infinite structure, rather than defining a completed infinite structure. Infinite structures cannot be completed.

With any inductive definition, you can get into trouble by naively treating the entire defined structure as a completed whole. Here we have, though, a particularly clear-cut case where there is no definition of the sequence at all; instead there is a finite specification of how to proceed with an unbounded nondeterministic process to generate elements of the sequence. The definition does not tell you what the nth element of the sequence will be; for that, you would have to actually carry the computation out to the nth step.

Real.[ ] is a perfectly good indeterminate Actor.

It doesn't seem vary useful though. A power series expansion for sin/cos, e seems much more useful, and capable of proving Euler's identity.

The problem with Real.[] is it may return Pi, but you will never be able to confirm that. All you know is it returns some real, and you may be able to test it is approximately Pi, but not prove it is exactly Pi.

Real.[ ] is useful to show that there are uncountably many Actors.

this can only be nonsense. WHAT are you talking about?

Some Actors computer programs, e.g., those of type Expression◅aType▻

The name of the song is called ‘Haddocks' Eyes.’”

“I was coming to that,” the Knight said. “The song really is ‘A-sitting On A Gate’: and the tune's my own invention.”

And expression of type real doesn't make the expression itself have the qualities of a real such as being uncountable.

Just naming your type as a member of reals doesn't have magical qualities.

Also I'm getting confused you're calling numbers actors now? Actors are supposed to be a model for computation where an actor is a point that recieves messages and sends them not the one name for everything you can think of.