Fixed points considered harmful

Fixed points have been an important topic ever since Church invented the lambda calculus in the early 1930s.

However, the existence of fixed points has unfortunate consequences:
* In a programming language, they preclude having having strong types
* In logic, they lead to inconsistency.

Fortunately, types intuitively preclude the existence of fixed points, e.g.,
ActorScript and Direct Logic.

Comment viewing options

Higher Order Functions.

Are functions first class in ActorScript? How can I pass an actor to an actor as a message?

Addresses of Actors can be sent in messages

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.

Y-Combinator

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: fixed points do not exist in ActorScript and Direct Logic

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

Can I create the Y-Combinator as a procedure?

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 in ActorScript

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?

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?

Y combinator *cannot* be defined in ActorScript

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]]


Well. I won't use Actorscript then.

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

The Y combinator is not practically useful for anything.

What nonsense

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.

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

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

Yah. But it works

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) ] 

Recursion + First Class Functions

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 Y combinator can't be implemented in ActorScript

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

Which is a great reason not to use ActorScript.

Which is a great reason not to use ActorScript.

If it's your own language why leave out "local recursion"?

"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 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.

What is not allowed?

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

Y fixed point procedure is not validly typed

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.

Not getting it

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.

Important for types that Y procedure definition is not valid

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

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

Nesting

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 has a definite definition: but no valid types

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

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?

Parameterized Y fixed point procedure: not typed

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]]


Why Y can't be defined in DL (simple) (re "not getting it")

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.

Simple function and Recursive Types

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>


Y fixed-point procedure is typed; but not its implementation

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

no recursive types re: Simple function and Recursive Types

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 σ1, σ2:Type then there is a function type: 1] ↦ σ2.

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.

Type System Using Big Lambda

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 uni"

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 Thomas!

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 ▮


Emacs abbrev file for DL & Actorscript?

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

Something Odd

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.

re Something Odd

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.

That's not it.

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.

Many functions

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.

Logic

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.

System F

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.

No universal quantifier

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/

Right

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.

How to express as a type system.

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


Just weaken System F

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.

Translation to logic

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

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.

Choosing

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

System F + ActorScript Types

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

Possible to define Fix◅aType▻

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.

Signature but no valid implementation of Y◅Sentence▻

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.

Separate thing

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.)

Martin-Löf, function identity, and polymorphism

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.

What does this have to do with software engineering?

I have no idea what's being talked about here, even though I know some perfectly good meanings for the phrase "fixed point". But even having no idea what's being said, I am ever more firmly of the opinion that none of this could ever have anything to do with the act of engineering software, which, after all, is what programming languages are for.

Can anyone explain, defend the proposition that there is anything here that could affect the actual implementation of software?

The bounds of logic define thebounds of reasoning about software

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.

Inconsistency Robustness: best we can do for large software

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

My software works.

My software works.

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

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

They don't

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.

A difference between tools and proofs

"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.

Mathematicians and logicians often get everything wrong

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.)

Everything in LTU is about types these days

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.

Scientists often concentrate on the trivial

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.

I suspect that mathematicians don't like algorithms

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

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.

Could you come up with examples?

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.

Prolog & Lambda Calculus

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.

I remember a talk...

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 initial enthusiasm for SAT solving has tempered

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.

SMT not just SAT

(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.

SAT, QBF, to SMT

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.

Many problems can be SAT-solved efficiently

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.

True, but also Cherry Picking

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.

I don't remember

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.

homoironic

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.

Yeah

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.

better metaprogramming

"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

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 done something along those lines

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.

I'm gonna add this to an existing language

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.

re: metaprogramming

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.

earlier than Lisp 1.5

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.

re earlier than lisp 1.5

That's an excellent resource.

minimum program size

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.

Name a language

after Andrey Kolmogorov.

utility of fixpoint combinators

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.

"with fixpoints we can use a simple macro expansion layer as an

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

macro expansion languages

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.

uhm

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

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".

I shouldn't get into this

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...

don't tease the sharp-witted human animals

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.

There are only a few people understanding Godel

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.

That thing that bugs me about Gödel

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.

contrapositive

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?

Yeah. But why?

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

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.

I get that

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

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?

Looks like cyclic reasoning to me

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?

What's the difference?

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).

Guess a difference of focus on Consistent and Complete Logic

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

The idea that mathematics

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.

One more attempt

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.

No. I got it.

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

Gödel's results invalid; Church/Turing proved incompleteness

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

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: Gödel's "self-ref" prop leads to inconsistency

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

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.

Do you understand the border of Consistent and Complete?

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?

NVM

I think I got it.

Wittgenstein: ⊢P and ⊢¬P where P is Gödel's "self-ref" prop

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

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?

Wittgenstein: Suppose ⊢⊬P; P is Gödel's “self-referential” prop

Hi James!

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


Regards,
Carl

Final response

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...

Wittgenstein: Gödel's "self-ref" prop leads to inconsistency

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

notation

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.

Direct Logic proves the 1st incompleteness theorem for ℕ

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

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

"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

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

I wouldn't know

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

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 am not entirely sure that you can do that

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

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.

Constructive procedures

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.

Yah well.

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.

Wittgenstein: "prove the improvability of P" means "⊢⊬P"

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

Assuming Godel's ⊢⊬"I am not provable." leads to inconsistency

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

I wouldn't worry too much

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.

Necessary to read an article in order to properly critique ;-)

John,

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

Regards,
Carl

Total FP for theorem-proving

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.)

No general recursion

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

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 math functions: different from executable procedures

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

Is that what he's saying?

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.

Termination

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?

Types are fundamental to programming languages

Types are fundamental to programming languages and consequently untyped programming languages are a mistake.

Fixed points hark back to the invention of programming languages in the lambda calculus and were used to show that the lambda calculus is a universal programming language for functions on numerals.

However, types mean that fixed points do not exist.

Some type systems permit fixed points.

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

The universal type does not exist.

Consequently, there are no fixed points.

Universal Quantification.

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?

Parameterized types

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]


Implicit Universal Quantification

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]


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


He probably needs at least the eager variant

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.

Lazy vs Eager

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

You need to think in the Operational Model

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.

fix and hi

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.

Y as a unary or dyadic combinator. And Hi.

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.

namespace (singular)

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.

Oh, no problem

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.

Implicit Universal Quantification 2

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.

Erroneous definition of the Y combinator

The following is not the definition of the Y combinator:


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


Missing the point

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 Y combinator

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]]


Incorrect

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?

The Y combinator *cannot* be defined using ActorScript

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.

Why is that?

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

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.

No fixed point implementation can be expressed in ActorScript

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.

Hewitt, you seem to avoid ...

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]


Doesn't this one 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

Hey! My fixpoint combinators are purrfect!

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!

re doesn't this one 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.

Direct Logic uses typed recursion instead of the Y combinator

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.

I almost see it

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....)

Types have raised very subtle issues ever since Russell

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.

re not talking about Goedel here

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.

Hah

so-called theorem

Now you're just trolling.

Not trolling: Gödel's "so-called theorem" 2nd Incompleteness

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.

So what

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.

"2nd Incompleteness" depended crucially on "I am not provable."

The problem is not that Gödel didn't present a formal proof. Gödel's "2nd 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 "2nd 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.

Discuss it with a logician

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.

Sigh

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

re Sigh

-

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).

His claim's are standard

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.

that's a cool hair to split (re his claims are standard)

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.

Meta-level claims

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.

meta-level claims and Goedel's 2nd

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.

Can assume number encoding

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 irrelevant to inferential incompleteness

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.

Not the Y fixed point procedure

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

Z combinator, then?

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.

Z combinator does not exist

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.

Lesser Rank

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).

re lesser rank

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.

Rank of types,

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.

Inconsistency-robust logic

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

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

Intuitionistic entailment is explosive

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

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

Explosion only to negated propositions

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.

Why not?

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.

Minimal logic

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

Proposition not Boolean; Peano induction predicate is Boolean^ℕ

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

Inconsistency Robust Type Checking

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

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

types constrain syntax

(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.

Not Boolean Then?

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?

propositions are expressions

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

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.

Propositions & Expressions.

Do propositions evaluate to expressions in DL?

Excluded Middle in Classical but not Inconsistency Robust 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

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

re that's not the definition i gave

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.

Working demo

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

d'oh! (re working demo)

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

re d'oh (corrected, I think.)

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.

Z is not very restrictive

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?

re 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.

That difficult-to-compute fixed point is nice

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.

Simpler

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

.

Y combinator has a definition (this is *not* the definition)

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

SingleArgument◅aType▻ ≡ [aType]↦aType

RossAngleY◅aType▻.[f:([SingleArgument◅aType▻]↦SingleArgument◅aType▻)]:SingleArgument◅aType▻ ≡
[x:aType]->(f.[RossAngleY◅aType▻.[f]]).[x]


Claim: There is no implementation of the untyped fixed point operator in ActorScript.

[Above edited for clarity and to fix a bug noticed by Ross Angle.]

Is it valid?

Is it valid ActorScript though?

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

ActorScript only exists on paper?

Can someone confirm this?

Practice lags behind theory

Currently, there is no publicly available implementation of ActorScript.

In theory, that is true.

In theory, that is true.

is that this is not the 'Y' combinator?

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.

re Y combinator has a defintion

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.

A Meta-Comment on Style

I'm not sure this is appropriate for LtU, but it's occurring so blatantly in this thread that a lesson seems worth drawing out into the open from it.

Carl is engaging here in a demand for rigor on the one hand while simultaneously engaging in hand-waving, hide-the-pea, and proof by strong assertion. It's plain to anyone reading the responses that this behavior undermines his credibility and effectiveness in the discussion. It's very hard to discern whether his responses are hand-waving bullsh*t or merely reflect an individual so deep into his thoughts that it is difficult to explain his assumptions and model.

The appearance of hand waving is self-defeating, and stature does not engender tolerance for it. It's a habit that all of us who are similarly afflicted should seek to abandon.

There is a cumulative effect to hand waving that warrants attention as well. When someone gives the appearance of hand waving pervasively, a very unpleasant question comes to insinuate itself into the minds of the listeners: "What part of this person's work, if any, can actually be believed?" At a minimum, the habit of hand waving drives listeners and readers to a more intensely skeptical view of everything the speaker says and has said.

Carl has done some truly superb work, and he has the intellectual and moral courage to delve with confidence into things that may turn out to fail spectacularly. That makes him a very rare researcher indeed, and much to be admired. Speaking solely for myself, it is distressing to realize that I view all of his results with stronger provisional skepticism because of interaction patterns like the one here.

Food for thought for myself, for Carl, and perhaps for others.

Finding ambiguities and addressing open issues

Dear shap,

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

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

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.

If Category Theory then ActorScript

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.

Formal semantics of ActorScript is in meta-constructs

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

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

Type checking rules of ActorScript are very strict

Type checking rules of ActorScript are very strict.

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

1 Corinthians 14

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.

Category theory is not much help in software engineering

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

Warning: high ferrous content in this message ;-)

I actually agree with that

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

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,

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 ;-)

Liked it very much (without the irony, this time)

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.

John: necessary to read & understand articles to critique them

Dear John,

It is necessary to read & understand scientific articles to properly critique them.

Regards,
Carl

Co-routines

Are co-routines possible in ActorScript? For example something like the infinite Fibonacci generator:

function fib() {
var x = 1;
var y = 1;
while (true) {
yield x;
var t = x + y;
x = y;
y = t;
}
}


Although we can rewrite this without the infinite loop and yield:

var fib = (function() {
var x = 1;
var y = 1;
return function() {
var t = x;
x = y;
y = x + t;
return t;
}
})();


I guess I am not clear how ActorScript handles mutation and closures?

What, formally, is "mathematics"?

Is there a single formal system (up to isomorphism) that deserves the proper name "mathematics"?

If I understand correctly (which is a dubious proposition), that is one of the starting questions from which Hewitt's recent publications can be understood.

A "formal system" in the sense I am using it here is a particularly strict set of rules with two key properties:

1. The rules proscribe a domain of discourse to which particular utterances can be definitely said to either belong or not belong.

2. The rules are decidable in the sense that a computer program can enumerate all possible utterances in order of increasing length and accurately report whether each utterance is or is not within the domani of discourse proscribed by the formal system.

What would it mean, then, for a formal system to be deserving of the name "mathematics"?

Speaking informally, a succession of specific historic developments have imposed some structure on rigorous mathematics. Mathematical discourse is structured around theories, each with its axioms, rules of inference, propositions, rules of negation, its proofs and theorems. Utterances and parts of utterances fall into these various categories. Each theory can be interpreted as a kind of set of construction rules, capable of producing utterances which are part of the theory, and those which are not.

Mathematics as a whole is evidently some generalized domain of discourse in which it is possible to lay out various theories. To compare the similarities and differences of their axiom sets, rules of inference and so on. It is one in which theories can be abstracted and subsumed to form results which depend only on certain aspects -- such as theorems abstracted over rules of inference that can be interpreted in any specific theory that happens to share those rules of inference.

And mathematics in this informal sense is inconsistency robust. In particular, the introduction of a new theory to the discursive domain, "mathematics", might be discovered to be inconsistent meaning the theory's discourse contains at least one proposition and its negation. Yet when this happens, all unrelated theories remain intact.

Notice that the discourse of mathematics itself does not exclude inconsistent theories. In fact they play a critical role It is common for the consistency of theories to be unknown but suspected. If a theory is inconsistent it is still a mathematical theory (albeit one with a bug). The proofs internal to the theory that demonstrate its inconsistency remain valid proofs. The theory may be inconsistent but mathematics as a whole remains robust.

A formal system deserving the name "mathematics" must evidently be one in which all of this reasoning about theories, and their relations, can take place -- including the discourse concerning the contents of inconsistent theories.

Past foundational attempts, such that of formalizing all of mathematics in ZF set theory, are not quite the same thing. Those past foundational attempts have in common that they tried to include in the span of the foundation all consistent theories, but specifically exclude all inconsistent theories. (The crisis of this approach was the discovery that consistency is, in the general case, not decidable.)

Hewitt's proposition is, in part, to construct a formal system which is capable of incorporating any theory, including all of its proofs, without regard to whether any particular theory is consistent or not.

Here is the catch though:

If you propose to me a formal system which you say should be called "mathematics", and if I can mathematically prove something about your formal system that can not be proved in your formal system, then clearly I have created mathematics that is not in your formalization. Thus your formalization should not be called "mathematics".

One of Hewitt's significant claims is that he has defined a formal system deserving of the name "mathematics" in that no formalizable theory can fail to be expressible in it, directly -- and at the same time the formal system itself, as a whole is inconsistency robust -- and at the same time every useful theorem about "mathematics" is directly expressible in the formal system called "mathematics".

[I find this increasingly plausible all of the sudden but I am not rigorously convinced yet, possibly because I don't understand it well enough].

Perhaps my account of the problem space, which I laid out above, might help others better understand the whole "fixpoints don't exist" stuff. On the one hand, syntactic restrictions (plausibly) prevent any formally constructed sentence in "math" from being defined by fixpoint. On the other hand, Hewitt challenges you to show one, even just one such fixpoint, defined outside of "mathematics", which would be useful to add to "mathematics" itself.

In other words, the point of the restriction is that if Hewit's utility challenge is correct, you will never find anything useful to say in mathematics that can't be expressed formally within "mathematics".

Confusion may be avoided

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.

re confusion may be avoided

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.

miscellany

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.

re ca 1900 and exclusion

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

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 nonexistent fixed point

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

avoiding Goedel (re a big part)

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).

Hmm

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.

re Hmmm

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?

sentences and proofs and theories

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.

re sentences and proofs and theoryies

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

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.

re The erasing happens

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.

More carefully

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 (⊧)

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!

Semantics

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.

Direct Logic is much more powerful than Tarskian set semantics

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 ℕ.

Proof?

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 semantics: can't deal with inference, e.g., soundness

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

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


Heh

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

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

You can be first ;-)

:)

Stronger than set theory re (heh)

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

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.

re If ⊢p doesn't assert the

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

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?

infinite sentences and math foundations

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.

Private Communications

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

re Private Communications

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.

Unconvinced

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.

re finite prefixes of the infinite bit string...

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.

Ok model, but the proofs?

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.

re Ok model, but the 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. :-)

backtracking somewhat

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 backtracking

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.

unconvinsing infinites: proofs, processes and "real" numbers

(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
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.

Actor descriptions vs. message values

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

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?)

undecidable theorems re hard time

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.

ah, different conception of "proof"

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.

re proof?

[...] 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

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 Ψ

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

Which axiom of DirectLogic

Which axiom of DirectLogic lets us tell the difference?

There is a Ψ: ⊧<sub>ℕ</sub>Ψ but not ⊢<sub>ℕ</sub>Ψ

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?

Erasure at top level

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.

Homework Assignment

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

re erasure at the top level

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.

Do you think I'm still missing something?

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.

a little, yes. re Do you think I'm still missing something?

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?

Thanks

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.

Each proof has a finite number of steps

Thanks for looking at the article.

Certainly, each proof has a finite number of steps :-)

re I don't see how a proof could ever be not checked finite time

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.

Oracles

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.

unerasable turnstile spotting (re Oracles)

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).

It could still mean truth

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".

Impossible to computationally enumerate the true prop of ℕ

It is impossible to computationally enumerate the true propositions of the Peano/Dedekind categorical axiomatization of ℕ.

Church's paradox: theorems of Math aren't computationally enum

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: provably true but unprovable propositions in *ℕ*

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.

re DL proves: true but unprovable propositions in *ℕ*

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: all true propositions of N can't be proved

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 N is very powerful

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 inexhautible

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.

exhaustive enumeration

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 syntactic formalism

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.

Trivial disproof

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.

fixpoints

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.

Incomplete

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.

fixpoints of procedures and "contra goedel"

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.

T inconsistent means ⊢<sub>T</sub>Ψ and ⊢<sub>T</sub> ¬Ψ

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.

Hewitt: OK

OK (re notation).

Re Hilbert's program being not entirely well defined: That's why they thought it was incredibly hard.

Struggling

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?

⊢<sub>T</sub> Ψ means that theory T infers proposition Ψ

T Ψ means that theory T infers propositon Ψ .

re struggling

What does "|- T" mean?

As Hewitt points out it means I created confusion by wrong notation. (re |-T). Sorry.

Goedel's method requires a fixed point

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

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.

re: "not entirely sure" and 2nd theorem

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

It's a theorem. It doesn't matter what you're using it for.

re it's a theorem

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

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).

Church/Turing incompleteness doesn't mean consistency unprovable

The Church/Turing inferential incompleteness theorem does not mean that consistency is unprovable.

re I'm not confused

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 or props

Types mean that fixed points don't exist for sentences; also they don't exist for propositions.

Consistency is possible for math theories but not completeness

Consistency is possible for practical classical mathematical theories but not inferential completeness.

re Goedel needs a fixed point

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

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-ref

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.

John, you're wrong about 2nd theorem

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

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" based on PM which had types (now corrected)

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).

Both right

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.)

John, I'd like to see your version of 2nd result

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

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".

Church/Turing incompleteness robust; Gödel's "proofs" fail

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.

re pattern in Hewitt's

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.

Yah. That's what you claimed before.

Still unconvinced one needs fixed points for the construction of Godel's argument.

burden re Still unconvinced one needs fixed points for the const

Still unconvinced one needs fixed points for the construction of Godel's argument.

That's on you.

Too Cheeky Nando's with the Lads

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.)

re too cheeky

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.

Arbitrary Side Condition

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.

proof sketch re: arbitrary side condition

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 Rn be an ordered list of sentences with one free variable. (Goedel calls these "class signs".)

Let Rn(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 (Rn(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 Rq

S == Rq

What is S specifically? Which "q"? S is:

S(n) := Rq(n) := n ∈ K == n ∈ { k in Nat. | ~Provable(Rk(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(Rq(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 := Rq(q)

equivalently:

X := q ∈ K where (X == Rq(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)

In Hewitt's system, this definition:

X := q ∈ K where (X == Rq(q))

is ruled out.

http://www.ursuletz.com/cs150-fall2005/lectures/goedel.pdf

In Direct Logic, sentences aren't countable; strings countable

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.

countability of sentences

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 Rn, a set of formula containing a single free variables.

The set Rn 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.

Gödel's argument for the 1st incompleteness theorem fails.

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.

Hah, Hewitt re: Gödel's argument for the 1st incompleteness ...

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 thm requires fixed point

Gödel's argument for 1st incompleteness theorem requires a fixed point.

re: Gödel's argument for 1st incompleteness thm requires fixed p

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

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

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, Church/Turing incompleteness is robust

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

re: one of the defects

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

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.

re: nonsensical

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

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?

re: Which paper do 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

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.

also John

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

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 foundations of CS

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.

Science is always a work in progress

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]


Whatever

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 appreciated for articles on HAL

Comments and suggestions gratefully appreciated for the articles on HAL.

Thanks!
Carl

It's just a joke

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.

Inconsistencies in mathematical foundations of CS are not a joke

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 :-(

Sounds unlikely

"they can lead to security holes"

https://xkcd.com/704/

Unlikely you can deduce my mother's phone number from 1=0 ;-)

It's unlikely you can deduce my mother's phone number from 1=0 ;-)

Yeah well. I am not a Platonist

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.

Until they prove otherwise

I would say does not have implications for security holes.

It sounds like bullshit.

What sounds like bullshit to you?

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.

When you're reasoning about computers, you're

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.

Define discrete math

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.

Does Godel apply to a totally finite system?

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.

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.

What's the conclusion or conclusions so far?

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?

 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?

Conclusions so far, IMO

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

"fixed points leads to inconsistencies in Mathematics."

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.

more "conclusions so far"

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.

Deeper issues to be addressed in inconsistency robust logic.

Thanks Thomas!

There are indeed deeper issues to be addressed in inconsistency robust logic.

How are you getting to "uncountable"

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"

 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.

"Wait till it comes around again how this relates to"

pervasively inconsistent networked information systems.

I don't believe this will relate to anything relevant to computers in my lifetime.

I know it's insulting

"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<sup>ℕ</sup>

Uncountablity comes from the type Boolean.

No there

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.

They seem deeply confused at what "uncountable" means

ℕ 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.

So even the address of a single actor takes infinite memory

:/
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. A computing machine is finite.

ℂ, ℍ, and ℝ are uncountable.

At given point in time, a physical machine will have a finite number of Actors.

Peano/Dedekind axiomatization of N is consistent but incomplete

The Peano/Dedekind categorical axiomatization of N is consistent but inferentially incomplete because there are true but unprovable propositions for N.

Not a recursive definition

[...] this definition:

X := q ∈ K where (X == Rq(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 == Rq(q)" meaninglessly tacked onto the side.

re Not a recursive definition

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 = Rq(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).

Missing each other's points?

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?

re missing points

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

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.

why did I define X that way

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 define X that way

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."

re *when* did you define X that way

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 Rq):

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).

Not recursive...

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 == Rq(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 = Rq(q))" is just some extraneous clarification. All it does is call to mind the alternative definition "X := Rq(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 = Rq(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?

What is S specifically? Which "q"? S is:

S(n) := Rq(n) := n ∈ K == n ∈ { k in Nat. | ~Provable(Rk(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 (Ri(n) == (n ∈ K))

S(n) := Rq(n)

Observe that (n ∈ K) == (n ∈ { k in Nat. | ~Provable(Rk(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 == Rq(q))

...this line is defining X as the proposition "q ∈ K." It's also observing that this is the same as saying X is Rq(q).

goedel's first theorm (pt 1 answer to Ross's correct criticism)

[Updated: Ross Angle pointed out a mistake in the definition of ParadoxFormuai 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), "Iformi(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 kth proof proves the nth sentence iFormn(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 ParadoxFormuai is not empty, then let:

  q := the least index of ParadoxFormulai


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 first theorm (pt 2 answer to Ross's correct criticism)

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.....

How are rules of construction violated?

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 IFormi(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.

Goedel's fixpoint (re How are the construction rules violated)

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 Iformi ∈ ℕ 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 Paradoxicali is an image of PotentialParadoxicali by the operation of self-application-of-index:

  Paradoxicali := PotentialParadoxicali(i)
for all i that are index of


If the family Paradoxicali 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 IFormi 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.

Lack of clarity in Sentence constructors (and nitpicks)

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 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?

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.

String must type check in order to be parsed into a sentence

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."

re (and nitpicks)

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, Iformi.

Here is a formula with x free:

  ~(x ∈ { j ∈ ℕ | ∃ k ∈ ℕ s.t. k iProves_self_applied_iForm j })


There is a subfamily of Iformi 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 PotentialParadoxicali is a subset of ℕ

The index set of the family Paradoxicali is the same as the index set of PotentialParadoxicali.

The family Paradoxicali defined in terms of a typical member is:

  Paradoxicali := PotentialParadoxicali(i)

== Iformi(i)
for all i in the index set of

== 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



Thanks, but what's the last part for?

Same up to alpha-renaming, yes.

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

effectiveness (re Thanks, but what's the last part for?)

Why do you then build up to this, though?

  Paradoxicali := Iformi(Paradoxical←Paradoxicali)


Just to emphasize that Paradoxicali is a specific family of fixed points.

(You can abstract the mention of Paradoxicali from the right hand side and install a fixpoint operator instead.)

Waving Hands and Daydreaming

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.

Church/Turing incompleteness theorem is not about arithmetic

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.

Direct Logic proof of consistency of Math is not dispositive

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

Direct Logic not part of mathematics?

Does this mean the proof of consistency of mathematics is contingent on Direct Logic not being part of mathematics? Yet it seems distinctly mathematical?

re Direct Logic not part...

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.

Proof of consistency of Direct Logic?

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?

Consistency hearsay and equivocation

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

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.

Math self-proof of consistency: convincing proofs maybe possible

The Mathematical self-proof of consistency shows that convincing proofs may be possible.

Math self-proof of consistency: common understanding inaccurate

The Mathematical self-proof of consistency shows that the current common understanding (based on Gödel's writings) is inaccurate.

Although Math can prove its own consistency, it may not be

Although Mathematics can prove its own consistency, it may turn out not to be consistent.

what is "mathematics" re Proof of consistency of DL

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".

Church/Turing proof of incompleteness has no fixed points

The Church/Turing proof of inferential incompleteness has no fixed points; but Gödel's "proofs" depend crucially on the existence of fixed points.

Gödel claimed to create a nonexistent mathematical proposition

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.

Interpreting Gödel, and meanwhile, F arithmetic

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

F arithmetic seems interesting. Here's a long thread from the n-category cafe discussing various weak models of arithmetic, including F.

Goedel's *second* theorem.

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".

Interesting

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 5 exists, then 3 exists

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

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.

F can't do that... maybe

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.")

Inference in Mathematics formalized using ⊢

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

what is "Computer Science"?

Every formal theory about computer programs or machines is presumably, generally speaking, of a mathematical character and thus, if Hewitt is correct, is expressible in his formal system, "mathematics".

Additionally, since very computer program is, in an important useful sense, itself a proof within the mathematical theory described by the programming language, each program is a proof within "mathematics" generally.

The (presumptively) directly apparent ability of Hewitt's foundation to express all these particular theories is (presumably) why he sometimes describes "mathematics" as the "foundation for computer science".

"mathematics" shows fixpoint sentences are a bad idea

Assuming my informal (but I think formalizable) understanding of Hewitt is right and is as he in intends:

It should be straightforward to build a convincing model of "mathematics" in which it can be shown that (if the model has fidelity) there is no sentence that contains its own encoding in the model itself. That is one way to restate Hewitt's claim about the role of types in preventing fixpoints.

It is further straightworward to extend the model with an additional modeled axiom that such a fixpoint exists (in particular a Goedel sentence). Goedel's second theorem shows us how to quickly show that the new modeled theory is inconsistent.

In that way, Hewitt's "mathematics" can demonstrate, via a model, that it should not be generalized to allow sentences which contain self-encodings.

At the same time, Hewitt's "mathematics" can (one gathers) easily demonstrate by model that it does not already contain any such sentence-with-self-encoding.

Object instantiation is the fixed point.

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" also *demonstrates* self consistency

The formalization of mathematics-in-general Hewitt plauibly says he's laid out contains a trivial and less than convincing (in isolation) self-consistency proof.

The system is (plausibly alleged) to be very easy to convincingly model in a way that makes it easy to prove the self-consitency within the model of formalized math-in-general.

The model is not a proof that the system expressing the model is self-consistent, but if the model is simple and mechanical enough the demonstration via model is anyway convincing.

Meanwhile, even though a new axiom can't be derived from the model's demonstration of the self-consistency of Hewitt's system, nevertheless that system already contains a self-consistency theorem more trivially arrived at.

The whole trick here is that do any but the most abstract math in Hewitt's system, additonal axioms have to be proposed in what amounts to a safely contained lexical scope.

Mathematics is founded on the categorical induction axiom

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.

Hewitt: incredibly lucid so far but...

What is going on at the top of page 15 of the Direct Logic paper?

Corollary: There is a proposition phi of Naturals....

Is the symbol for Naturals there a typo for tau?

What is the double-bar turnstile thing?

Hewitt: concs

Are we grown up enough to live with uncertainties or will we repeat the mistakes of the twentieth century and pledge blind allegiance to another certainty. Malone [2007]The world always needs heretics to challenge the prevailing orthodoxies. We are lucky that we can be heretics today without any danger of being burned at the stake. But unfortunately I am an old heretic. Old heretics do not cut much ice. When you hear an old heretic talking, you always say, “Too bad he has lost his marbles.”

I'm sorry I was one tending towards that conclusion. On the bright side, it's a really interesting experience to discover one was wrong about that -- to see from both sides what that's like.

Thanks!

Carl

Hewitt: appendix question

Third line of type definitions on page 26 (DL paper): "If f:Type^Nat ..."

I don't know what the notation is trying to say and the footnote isn't helping.

update: No it's not a typo. I got it, now.

semantics for DL & answer for Matt M.

DL appears to have a natural, weak, operational semantics. (Matt M., at the end I address your "truth oracle".)

Looking at DL this way helps to clear up the difference in DL between provability and truth.

It also illustrates an interesting oddity: the provability of a theorem in DL is not always well defined! In other words, DL semantics under-determines theorem provability in some cases.

In this operational semantics, the meaning of a proposed proof is a computation that can return True if the proof is verified, False if a mistake is found, and in some cases the program must diverge rather than returning anything.

To illustrate, consider the proposition, containing two literal real numbers:

φ ≡ 3.1415.... = 3.1415....


Is it provable?

⊢? φ


It is such a simple proposition that we expect it to be self-proving or self refuting. For example with integers we get:

Theorem: ⊦ 2 ≠ 3

Proof

1. 2 ≠ 3     by inspection
2. ⊢ 2 ≠ 3   by 1 and Adequacy


Theorem: ⊦ φ
where a ≡ 3.1415...
b ≡ 3.1415...
φ ≡ a = b

Proof

1. a ≠ b   by inspection?!???!!?
Note: step 1 raises a tricky problem.

2. ⊢ φ   by 1 and Adequacy


The two real numbers in φ are actual real numbers. For example, they may both be infinite, lazy lists of digits (and one decimal point) produced by Actors.

We can not glibly assume that any two arbitrary reals can be found equal "by inspection".

So what is the semantics of "=" in this context?

In this case "=" has a natural inductive definition -- and dual induction on the two infinite lists of digits.

Suppose that RComp is a procedure that performs that inductive equality test. A naive implementation of RComp would simply compare successive digits of the two infinite lists of digits. It would return only if the two reals are found to be unequal.

In some environments, it would be possible to write versions of RComp that can sometimes return True when the two reals are equal. For example, an implementation might (behind the scenes) notice that both real numbers are a standard Actor that returns 0, exactly: 0.000....

It is fine for an implementation of RComp to return True in finite time so long as it does so faithfully. The semantics of "=" are given by an inductive definition. RComp is free to recognize the induction holds in whatever special cases it can.

Given this, we can write the proof:

∀ x,y ∈ ℝ (x = y) ⬄ RComp[x,y]


So:

Theorem: ⊦ φ
where a ≡ 3.1415...
b ≡ 3.1415...
φ ≡ a = b

Proof

1. RComp[a,b] = True   by inspection?!???!!?
Note: step 1 still raises a tricky problem.

2. ⊢ φ   by 1 and Adequacy


And this suggests some semantics:

The proof is valid if the reals a and b happen to be unequal. That is because we can certainly identify them as unequal "by inspection", looking at only a finite number of digits.

The proof is valid if the reals a and b turn out to be of a kind that some (correct) implementation of RComp returns True in finite time.

Otherwise, the proof is not valid, which is to say we do not obtain ⊢ φ.

We also do not obtain: ⊬ φ.

This is not, however, the same thing as a case of inferential incompleteness. In particular, suppose that no valid proof of φ can be found. It is not the case that we can assume ⊫ φ.

For example, if behind the scenes both a and b are copies of a single random stream of digits they will be, in fact, equal. It is not safe to assume they are not equal for from that we could infer the existence of digits where they differ. And if they are equal but no proof can ever show it, we can not assume they are equal because from the deduction rule Adequacy we could infer a valid proof could be found.

Here then is how the semantics I'm describing sort out truth and provability in DL:

That which we know to be true is provable. ("Adequacy").

That which is provable we know to be true. ("Soundness").

"provable" is established by demonstration and means that a proposed proof has been checked in finite space and time. A "valid proof" is one that can be checked in finite space and time.

It is possible to construct propositions whose truth ("⊨") is definite but unknowable. (As described above.)

Wrongly assuming the falsehood of an unknowable truth introduces error. (Such as the error of assuming a valid proof exists.)

Matt M. suggested that a model for DL could follow by assuming there are no unknowable truths. For example, we could imagine an oracle that can always, instantly tell us if two reals are equal.

Oracles of that sort lead to paradox. For example, given such oracles, DL would be able to define an enumeration of all programs that halt.

Why parameterize propositions with values?

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.

re Why parameterize propositions with values?

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.

Don't see it

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?

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.

re where's the proof

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?

Same question

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.

re same question

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.

re Apparently, I can just claim this equality as a single proof

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.

Computable sentences

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.

actor programs are nondeterministic

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.

Good stopping point :)

I'm unconvinced, but we'll see.

Inferring that x=y in Mathematics requires an actual proof ;-)

Inferring that x=y in Mathematics requires an actual proof ;-)

A single Actor definition

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'.

metaphor, cognition, and infinity

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.

nondeterminism (re a single Actor definition)

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

By a diagonal argument, there are uncountably many Actors.

See page 10 of Inconsistency Robustness in Foundations

interplay of denotation and real state (re non-determinism...)

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

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 Actors

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.

Sure.

Given infinite time.

My ex does this too.

My ex does this too.

if you have reals (infinite memory) and the time to distinguish reals (infinite time).

Nonsense.

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.

cakes relevant to mathematicians

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.

Okay.

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).

uncoutable distinct

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?

physical implies finite time

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.

definition specifies vs. # of runs

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.)

non-physical mathematical idealizations

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).

source text vs. manifestation

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

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, an Actor real nonelement of set

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.

Underlying disagreement

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.

re The real disagreement is as to what exactly the "set of outpu

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?

which real is it? (physically speaking)

A machine can decide equality between two physically manifest reals by comparing their bits, or by comparing their actor addresses, or by some combination.

You people are driving me crazy

A computer with infinite memory and infinite time is not a computer. What are you on about?

Josh your misunderstanding is in this vicinity

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.

In that case

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.

What's going on here anyway?

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.

Better

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.)

Thank you

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.

 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?

unbounded or infinite time

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

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.

re "The constant denoted"

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

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.

re" "only way we can prove useful identities of reals"

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.

Algebraic manipulation of power series.

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.

re algebraic manipulation

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

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.

re confronted with...

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

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

Real.[ ] is a perfectly good indeterminate Actor.

Not very useful though

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 there are uncountably many Actors

Real.[ ] is useful to show that there are uncountably many Actors.

If an actor is a computer program, then

this can only be nonsense. WHAT are you talking about?

Some Actors computer programs, e.g., of type Expression◅aType▻

Some Actors computer programs, e.g., those of type Expression◅aType▻

The name of the song is called ‘Haddocks' Eyes.’”

“Oh, that's the name of the song, is it?" Alice said, trying to feel interested.

“No, you don't understand,” the Knight said, looking a little vexed. “That's what the name is called. The name really is ‘The Aged Aged Man.’”

“Then I ought to have said ‘That's what the song is called’?” Alice corrected herself.

“No, you oughtn't: that's quite another thing! The song is called ‘Ways And Means’: but that's only what it's called, you know!”

“Well, what is the song, then?” said Alice, who was by this time completely bewildered.

“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.

Since you are into Lewis C.

Your language policing is less interesting than constructive dialog about what is actually being said. You could regard yourself as, in this context, trying to pick up a new language (both formal and with colloquialisms) by immersion.

A program that spits out random digits

is pretty much the only way you can (sort of get) the reals out of a computer program.

But that doesn't make actors uncountable, because one result from an actor is not an actor, it's a result.

You're confusing levels. The song is not the name of the song.

The expression is not itself a member of the type of the expression.

Josh: rigor (2)

You're confusing levels.

I have no idea what you mean by a "level".

But that doesn't make actors uncountable,

The set of actors denoted by a an actor program is, for some programs, uncountable. The definition given for "Real.[]" is an example.

The expression is not itself a member of the type of the expression.

Uncountable Sentences are formally defined. Have you read the paper? Where did you get stuck?

God, I give up

I looked up the definition of "Real.[ ]"

It's exactly what I thought it was. It can spit out one indeterminate real and never finish...

You're calling the infinite result of "Real.[ ]" an actor? Uhm no? "Real.[ ]" is an actor, its result is a string of 0s and 1s.

If you call everything everything then yes, you have a wonderfully impressive mysticism. And you accusing me of lacking rigor?

Pretty much.

Once again

"Real.[ ] is useful to show that there are uncountably many Actors."

Uhm no. It shows that you can get an infinite string of random digits out of an actor.

The way to get from that to "uncountable actors" is missing.

How do you show that an unfinished result is "an actor"

Josh have you read the paper? Where did you get stuck?

re: "this can only be nonsense. WHAT are you talking about?"

re why aren't you applying your...

By coincidence I think my very recent reply to a different comment responds to your point here.

I'd previously read that other reply to a different comment. I don't think it has any bearing. You talk there about two things being aspects of the same "thing", but I don't see that there's a "thing" there for them to be aspects of, whatever one ought to mean by "aspect" in this context. Btw, something went awry with your apparent attempt to define the reals by induction and a related set of equivalence classes; and I suspect this isn't a technicality, but instead may get at what you're missing about the difference between enumerations and completed structures (but I'm not exactly sure what you're missing). You haven't defined the real numbers (in the interval), nor even defined the rational numbers; you've defined by induction the rationals that have a finite binary representation, i.e., those whose denominator is a power of two. Any rational number whose denominator isn't a power of two does not correspond to any equivalence class there. For example, 1/3.

Btw, something went awry with your apparent attempt to define the reals by induction [....] Any rational number whose denominator isn't a power of two does not correspond to any equivalence class there. For example, 1/3.

I cleaned it up in a new topic post.

"Dedekind, Cantor, Conway, & Hewitt (w/ some Chomsky)"

There, I construct the reals in terms of partitions of sets of finite bitstrings, drawing out a correspondence of rationals to regular languages, constructible reals to recursively enumerable languages, and reals in general languages defined as prefixes of an unbounded history of coin flips. There is a clear relation to Dedekind and Conway and the construction I give is basically a paraphrase of Hewitt's construction of Real.

Have fun. I think It's cool. Sincerely for real and for true, mate.

Validity (i.e., correctness) of proofs is decidable

There is a computable total procedure Proof? such that
∀[p:Proof, s:Sentence]→ ├p ⌊s⌋ ⇔ Proof?.[p, s]=True

validity of proofs

There is a computable total procedure Proof? such that
∀[p:Proof, s:Sentence]→ ├p ⌊s⌋ ⇔ Proof?.[p, s]=True

I should pick a different word from validity then.

Your concept is a computable total procedure that checks whether the form of a proof is correct. That can be done in finite time.

I guess I should say verified, then.

Verifying a proof means inspecting it to see if assertions made by inspection are accurate (such as an assertion of equality between two reals).

What is a proof?

Somehow you have a total procedure to verify proofs but you can't enumerate all proofs, then, right? Because if you can enumerate proofs and you can check their validity, then you can enumerate theorems.

These proofs must be abstract entities, I guess, that somehow witness the truth of sentences? I don't know... none of this makes any sense to me. If your proofs aren't actual proofs, then it doesn't seem truthful to read "├ Ψ" as asserting the provability of Ψ.

as I see it: re What is a proof?

Taking constants as atomic, all sentences are finite. All proofs are finite. This is because they are inductively constructed in finite numbers of steps.

If we take judgements such as testing the equality of constants as a total procedure, Proof? is a total procedure.

Not all constants contain a finite amount of information. The one-line Actor construction on page 10 (infinite random stream of bits) illustrates that.

In an operational model, Proof? may not terminate, even though it appears total taking constants as atomic and equality of constants as a total procedure.

So there is a hair that could be split here between a procedure defined within DL that is abstractly total, and an implementation of DL in which a faithful implementation of that total procedure must not (in the general case) terminate for all inputs (but must terminate for some).

Ok

So if we restrict to the subset of DirectLogic that coincides roughly with second order logic, we can enumerate the sentences but not the proofs, because some of those might contain actors and there might be uncountably many of them.

Maybe that is what he has in mind. He can always clarify. It sounds like the model I had in mind isn't going to work with the axiom Hewitt just produced. I'm not going to try to think of another model, though. I will say that none of the things Hewitt is doing seem to have the flavor of increasing consistency strength of the system. I suspect it will either have a relatively straightforward set theoretic model or will be inconsistent. I could be wrong.

not (re) OK

There are uncountably many Sentences in DL.

"Proof?" is a total computable proc; theorems of Math not enum

"Proof?" is a total computable procedure but the theorems of Mathematics are not computationally enumerable.

⊢<sub>ℕ</sub>Consistent[ℕ]: open problem in Math

Consistent[ℕ] is a fundamental open problem in (Meta-)Mathematics for the Peano/Dedekind axiomatically defined categorical closed theory ℕ where Consistent[ℕ] means that no contradiction can be derived from the axioms and rules of inference of ℕ.

Arbitrary Reals Do Not Exist

I think this is interesting, however I am not sure I see the point, or see it as something fundamental yet. Surely 3.141... = 3.141... if the generating expressions are equal. In this case we might have a symbol Pi that represents this number, and we can clearly say Pi = Pi with no problems. e^(i * Pi) = -1 is an important identity, and relies on Euler's formula, which reduces to a series limit (remember I mentioned Zeno's paradox). So we should be able to represent such reals as power series expansions, and evaluate the limits of such series. There are several series that converge to Pi, and any system for mathematics must recognise their equality.

Personally I think the answer is that the reals should not exist in the system. You cannot create a real number by enumerating digits as you will stop at some finite precision number before the universe ends.All other reals should be represented by the equation that generates them, and equality can be proved by a transformational proof on the equation only. So we can prove e^(i * x) = cos x + i * sin x by power series expansion for example.

how to construct an arbitrary real

The real numbers in the range [0,1] are isomorphic to their infinite binary expansion. I.e., 0 is an infinite list of 0 bits. 1 is an infinite list of 1 bits. 1/2 is a list with a 1 bit first, then infinite 0 bits.

As a notation, you could write 1/2 (an infinite list of 0s preceded by a 1) on paper, like this: 1‾0

3/4 = 11‾0

1 = ‾1

1/3 = ‾ 01

What's going on here is that there is enough regularity in those binary expansions for you to reason about them inductively, very easily.

In this age of miracle and wonder you could also denote a unique real number with an active device. Picture a little box with a button. When you push the button it displays a 0 or a 1, the next digit in some real number.

Perhaps the digits a given device produces are deterministic or perhaps they are random. It makes no difference.

Suppose we have a device that produces random digits.

Does that device represent a specific real number, one that incidentally is (with probability 1) a non-constrable real?

On the one hand you could say that the real number we're thinking of "doesn't exist" since we will never be able to examine all of its digits.

On the other hand you could say that the real number indicated by that device certainly does exist, in the sense that any assertion made about its nth digit can be verified or refuted by inspection.

Here is a practical consideration:

We can use the mathematics of real numbers to reason about the output of this device, even though we can prove fewer facts about the number than if it were a known, constractable real.

Why not then, as DL does, allow numbers such as this to appear as constant terms in abstract Sentences?

If your foundational theory makes it easy to allow such numbers, even if you could remove them from consideration in a sub-theory, isn't that a virtue of your foundational theory? The virtue being that it recognizes and makes useful the commonality between such output signals of random bits, and abstract real numbers?

Rational numbers are fine.

Rational numbers are not real numbers. So a/b where a and b are finite integers are rational. No problem with these numbers, and you represent them as fractions.

Your representation is just another finite domain, and if you could define addition and multiplication you could have an algebraic group. The maths of this finite domain does not require reals, just like the maths of rational numbers does not require reals.

The device cannot output a real number, when the universe ends, it will have output a finite number of digits, and this number will be rational.

Only special reals like Pi and 'e' actually exist, and they are the output of symbolic equations. It is vital we can establish the identity of all the different symbolic generators of Pi. The only way I know to do this is by algebraic manipulation of the pure generator functions.

rational numbers are fine

The device cannot output a real number, when the universe ends, it will have output a finite number of digits, and this number will be rational.

You can take this approach but if you do, you will need a thoroughly finitary foundational theory.

For example, applying your principle, we can not use the classical natural numbers. Instead, we must assume that there is some finite largest integer.

If you are not prepared to make such a drastic commitment, then you may not accuse my digit-generating box of being a rational number, because that will lead to falsehoods. In particular, you will be able to falsely prove the existence of some specific rational, but I will be able in principle (with probability 1, at least) to show that you have produced a contradiction and your system is inconsistent.

Not really

I don't think a foundational logic needs an infinite set of objects representing the real numbers.

think that through (re not really)

I don't think a foundational logic needs an infinite set of objects representing the real numbers.

Interesting theory. Do you have a write up of it?

You are in (I think) good

You are in (I think) good company: MF118: Real fish, real numbers, real jobs. (The connection to real numbers comes around the five minute mark.)

That might not be the best first introduction to this like-mind mathematician so here is a link to his (ongoing) series that deals with this and other number math (not logic) issues: MathFoundations. There are over one hundred videos on very specific topics. If the first one that I linked is not interesting perhaps one of the other ones will be.

you may not accuse my

you may not accuse my digit-generating box of being a rational number because that will lead to falsehoods

If your digit generating box has a finite size, i.e. a finite number of states, and only a single event input, then it will certainly generate a rational number.

It'll certainly never

It'll certainly never generate an irrational number, since the output would only be irrational if the box had finished generating an infinite number of digits, which won't happen by the definition of "infinite".

re: it'll certainly never

It'll certainly never generate an irrational number, since the output would only be irrational if the box had finished generating an infinite number of digits, which won't happen by the definition of "infinite".

Anyone is certainly welcome to propose a foundation of mathematics for computer science in which there are no uncountable classes of object. It could be interesting. Instead of saying "fixpoints don't exist in mathematics" you could be the one saying "turing machines don't exist in mathematics; neither does lambda calculus".

This has nothing whatever to

This has nothing whatever to do with uncountable classes of object. This is about using infinities as an excuse to not bother to define things, which makes it possible to make arbitrary and ultimately meaningless claims. Completed infinities are one of the ways of viewing the meltdown that befell mathematical foundations (one impression of the elephant), and it does seem Hewitt has failed to realize he's introduced an even more virulent foundational failure than the ones he claims to have eliminated (setting aside the question of whether he actually eliminated them, or of whether eliminating them does what he thinks it does; note, I've not forgotten I'm to take a look at the paper you recommended).

This is about using infinities as an excuse to not bother to define things, which makes it possible to make arbitrary and ultimately meaningless claims.

Fine. That is an interesting assertion. I think it is not a fair description of the work under consideration but I could be wrong.

Let us explore the question.

What specifically is it that you think has not been defined? Or a specific example thereof? Perhaps I can be convinced you are right or perhaps I can fill in a gap for you.

Doubts concerning the

Doubts concerning the foundations of mathematics pretty much start at infinities and spiral out from there. Remember that quote attributed to Kronecker, "God made the integers, all else is the work of man"? Starting point. The basic objection to the Law of the Excluded Middle (another view of the elephant) is that it applies only to completed, which is to say finite, structures. Russell and Whitehead avoid impredicative definitions by requiring any particular definition to contain only a finite depth of nesting of other definitions, i.e., a finite type (another view of the elephant). And, just to make a clean sweep of the three schools of thought, Hilbert's meta-mathematics is finitistic (sometimes called finitary). Finiteness, completion, is the heart of the whole thing; it's the essence of the concept of proof; "infinite proof" isn't an oxymoron, it's a contradiction in terms.

You ask for specifics. Makes sense, from your perspective. From my perspective, there's an efficient way to pursue such specifics, and an inefficient way. Efficient is to read Hewitt's paper (the one you recommended) directly, if one is going to do this at all. I said I would, and my intention has not changed — out of respect to you, not to Hewitt who started out with some credibility on which to earn a fair hearing and has proceeded to squander it. If you are overlooking something, I would expect it to be, most likely, an intelligent mistake resulting from looking for more sense beneath Hewitt's work than is actually there.

hint (re infinite proofs)

Finiteness, completion, is the heart of the whole thing; it's the essence of the concept of proof; "infinite proof" isn't an oxymoron, it's a contradiction in terms.

There aren't any "infinite proofs" in DL but there are some constants that contain a countably infinite amount of information.

There aren't any "infinite

There aren't any "infinite proofs" in DL.

I didn't say there were, and reserve judgement on that specific technical point, though noting the techical point may turn out to be slippery.

insult is not argumentation

Hewitt has failed to realize he's introduced an even more virulent foundational failure than the ones he claims to have eliminated

see above

See above. (Note: I have no interest in arguing, as well as no interest in insulting. If I think a line of reasoning is invalid, I mean say so; not an insult, just a statement. I do try to be careful to qualify my statements, a care that appears to have gotten lost with trimmed context in this case.)

transcendental darts

A fun, short video on this subject: Transcendental Darts (by Vi Hart).

Suppose we have a device that produces random digits.

I'm not convinced this is a sound assumption. Can non-deterministic random devices physically exist? How would you know?

In any case, such a device would not exist in any finite expression of a deterministic logic/math/PL. Nor could it be a physical finite state machine.

As far as I'm concerned, most real numbers aren't. Yet, there are some useful numbers outside the rationals, such as pi (which can be expressed in a finite program) and sqrt(2) (which can be expressed with an appropriate notation).

Though, I'm interested in rational trigonometry [tutorials] because I like rational numbers much more than roots.

Why not then, as DL does, allow numbers such as this to appear as constant terms in abstract Sentences?

I can think of at least a couple reasons I wouldn't want infinite sentences in my logic:

• I cannot determine in finite time when two arbitrary, infinite sentences are structurally identical. Consequently, you cannot always determine whether sentences contradict each other (e.g. X = 01001010...., Y = 01001010...., X =/= Y; do these contradict? inspect possibly forever to find out!)
• I cannot generally compose such sentences - e.g. if I add or subtract two real numbers expressed as an infinite series of digits, there are problematic edge cases where I cannot compute a carry value without an infinite computation.

One might reasonably argue an infinite sequence of digits isn't a valid representation of a real number because real numbers are well ordered and closed over addition, subtraction, multiplication... but the infinite series is not closed (due to divergence for carry values in edge cases) and not well ordered (you can't generally compute a least element due to divergence in comparisons).

"Real" numbers

Whether the real numbers are or aren't real isn't important. The question is whether reasoning about them leads to contradiction. As long as it doesn't, they're simpler than the alternative.

we can prove that, using math (re transcendental darts)

Can non-deterministic random devices physically exist? How would you know?

It follows from three physics hypotheses. Two of these hypotheses are among the best confirmed empirical results in the history of laboratory physics. The third hypothesis is not empirically falsifiable but amounts to a belief that information travels no faster than the speed of light. (Conway and Kochen's FWT, of course..)

More simply, though, it is trivial to build random number generators based on quantum noise that pass all known tests of randomness.

In any case, such a device would not exist in any finite expression of a deterministic logic/math/PL.

Correct. That is among the reasons Direct Logic distinguishes between strings and Sentences.

As far as I'm concerned, most real numbers aren't.

I won't deprive you of that view. As I said, one can say such numbers don't exist because we can't manifest them in full. And one can say that such numbers do exist because we can produce examples with the property that we can examine any digit of them we choose to examine.

I cannot determine in finite time when two arbitrary, infinite sentences are structurally identical. Consequently, you cannot always determine whether sentences contradict each other

Correct. Not "always".

I cannot generally compose such sentences - e.g. if I add or subtract two real numbers expressed as an infinite series of digits, there are problematic edge cases where I cannot compute a carry value without an infinite computation.

Correct. There are uncountably many such cases.

We can prove that. Using math.

can't examine any digit

And one can say that such numbers do exist because we can produce examples with the property that we can examine any digit of them we choose to examine.

If I were to say, "I have this monad with excellent properties so long as you don't use 'bind'...", one might reasonably argue: "well, that's not really a property of your monad, then."

I feel this applies to your example. "I have these numbers with a nice property, that you can inspect any digit, so long as you don't use 'add' (or compare, or anything else, really)." If you do add two numbers, you might be unable to examine even the first digit.

It isn't merely an issue of manifesting numbers 'in full'. Outside of an algebraic context where we can compare or compose numbers, all you really have is 'infinite strings'. Infinite strings, even if you limit their alphabet to a set of popular digits, simply aren't the same concept as numbers.

More simply, though, it is trivial to build random number generators based on quantum noise that pass all known tests of randomness.

We can also trivially create secure deterministic finite-state pseudo-random number generators that will pass all known tests of randomness until well beyond the heat death of the universe. :)

I'm not convinced even the best of our empirical experiments have isolated enough variables to determine whether behavior is non-deterministic. We're still trying to understand gravity, and we don't really know whether there is a deterministic theory behind quantum noise and coupling that is beyond our direct observation.

A couple years back I read this gem which purports to greatly simplify a variety of quantum interactions (e.g. compared to Feynman diagrams) by placing them into a timeless multi-dimensional structure. Someone else (on reddit, I think) commented that they were working on a similar theory, but with four more dimensions, that covered even more interactions. I haven't kept up, but I'm curious what will become of these.

mathematics for computer science

I feel this applies to your example. "I have these numbers with a nice property, that you can inspect any digit, so long as you don't use 'add' (or compare, or anything else, really)." If you do add two numbers, you might be unable to examine even the first digit.

Correct.

Of course, the sum is still perfectly well defined by a kind of structural induction.

timeless multi-dimensional structure.

Of human interest is what we know when.

re: math for cs

Of course, the sum is still perfectly well defined by a kind of structural induction

Divergence seems a rather large imperfection to overlook. Structural induction on a coinductive or infinite structure isn't well defined in every logic.

Getting back to the topic of a math or logic for computer science, a reasonable question is whether our logic should accept as well defined a sum over infinite strings (or the infinite strings themselves).

Infinity

I can say 9.9... plus 0.0...1 is 10 but again I have created a new symbolic representation with its own algebraic properties.

What is interesting is mathematical identity has no concept of time. A = B implies A and B have always been and will always be the same. Two things are identical whether or not we have discovered the proof of such yet. The value of Pi existed and was Pi before we calculated it.

I think this is a fundamental difference to computability which does involve time. We cannot compute Pi (completely) but we do know mathematically that "sin Pi = 0". Reality is finite, and reality is computable. Reality is consistent but not complete (as is what is computable).

But we can compute proofs (as we agree they must be finite). That is the key. The timeless nature of equality let's us symbolically manipulate abstractions. For example sqrt(2) does not exist, it is not real, it cannot be computed and does not exist in reality. But we can construct the abstraction of square numbers, and we can extrapolate from this what the square root is. We can construct an abstract representation of such numbers which is finite, and compute using that.

My thinking would be that infinity has to be a fundamental concept in the system, as do some kind of recursive definitions. We should be able to represent series like "sum(n is 1 .. infinity) [1/n]" and know that it's value is 2 and operate algebraically on such series in finite time (such as adding two series). Mathematica seems to do this quite well whilst running on a computer with no irrational numbers.

This would suggest we need fixed points and infinity, but not uncountable objects, such a thing is not computable and does not exist. The fact that irrational numbers are not real, and I cannot store one in my memory strongly suggests they are not foundational.

Sand Castles

Somehow this discussion reminds me of two crazy naked philosophers sitting on the beach in sand castles while a flood is coming while bickering about that their own sand castle will withstand the flood and the other party got it totally wrong.

Never mind me. I am just enjoying the sunset.

Waiting For Godel

Isn't there a play about that: "Waiting for Godel"?

Unfortunately, Terry

Unfortunately, Terry Pratchett died. Otherwise he could have written a great book or play about people here.

Cheers,
Carl

Thomas: thanks for noticing the typo

Thomas,

Thanks for noticing that end note 10 repeats end note 9 in
Classical Direct Logic

Cheers,
Carl

-

Posted in wrong place.

defining reals

The custom when talking about real numbers is to mention an integer part and a fractional part. Here is an alternative:


Constructing the reals:

"0." is a real approximation

If "0.X" is a real approximation then so is "0.X1"

If "0.X" is a real approximation then "0.X0" is an incomplete real approximation.

If 0.X0 is an incomplete real approximation, then so is 0.X00.

If 0.X0 is an incomplete real approximation then 0.X01 is a real approximation.

Note that if 0.X is a real approximation then 0.X is also a dyadic rational.

The dyadic rationals are well ordered.

"0." is a real number (not only a real approximation).

"1." is a real number and is also a dyadic fraction.

Every dyadic rational is also a real number.

If "0.X1" is a real number then the set of all dyadic fractions less than "0.X1" is also a real number.

If Y is a real number, then the set of all dyadic fractions greater than Y is also a real number.



That is the logical structure of the output described by Hewitt's one-line Actor-definition, constructively expressed in terms of sets, with no reference to a stepwise program-evaluation concept of time.

You have no intention of responding to any of my

questions about how sentences or actors can be uncountable.

I guess I'm not worthy, eh?

Appropos of nothing

Maybe if we're going to have theories about computer science phrases like "uncountable infinities" should be considered evidence that we've gone off track.

Maybe we should start with finite model theories, finite arithmetic and numerical approximations and only go beyond those if absolutely necessary.

Has anyone ever needed the axiom of choice for a computer program?

Logic, Neurons and Godel Numbers

Here's a presentation about the relation between logic and neural networks:
http://staff.computing.dundee.ac.uk/katya/UK.pdf
Whilst the topic of the paper itself is interesting, I think there is some important stuff here.

You cannot prohibit Godel numbering. The numbers are not assigned by the logic system, but by the observer (in this case the neural net, but in our case the human brain). The argument that real numbers prohibit Godel numbering by being infinite is shallow. I can represent a real number by a single "Godel number" standing for each unique real in the formula (as I cannot know the actual numbers, the fact that they are unique is all that is important). Effectively we just need a unique variable for each real and use De Bruijn numbering. To know a real we must know the generator equation, in which case we can Godel number the generator equation and subtitute this for the real number. Any argument about systematically prohibiting this is void because the numbering happens in the (human) observer not in the logic itself. The key point is to understand the number is the observers internal representation of the logic. Any arithmetic then performed on this is then just the observers intuitive arithmetic and outside the system under consideration. I'm not really saying anything about the applicability of the incompleteness theorems, just the specific point of Reals breaking Godel numbering. The observers neural net is finite, therefore all maths must have a finite representation in the neural net, and that is what we assign the Godel number to.

Strings are countable but sentences and propositions are not

By a famous proof due to Cantor, the real numbers are not countable.

Consequently, strings are countable but sentences and propositions are not. Hence, Gödel numbers are only applicable to strings.

Doesn't likely block the construction of a Goedel sentence

Uncountabilty doesn't likely block the construction of a Goedel sentence. I can simply restrict myself to that part of the syntax which I can write down.

Maybe something else blocks the definition of a Goedel sentence but this isn't it.

It's gobbleldygook

The only way that "sentences and propositions" can be uncountable is if you allow infinitely long sentences and propositions.

How is that useful or necessary?

The only way that "sentences

The only way that "sentences and propositions" can be uncountable is if you allow infinitely long sentences and propositions.

They can also be uncountable if you allow a single token to contain an infinite amount of information. Which is also neither useful nor necessary. But of course it's all irrelevant to Gödel's results, since those results only need the finite parts of the theory to exist, regardless of whether you choose to assume infinite stuff "exists" too.

uncountably many sentences

Some people think of math as a kind of language of finite strings drawn over finite alphabets. (Some would say "countable alphabets" but, without loss of generality, we can assume finite alphabets.)

A typical construction begins with a grammar for propositions which might be parsed as expressions and sub-expressions with primitive terms, drawn from the finite alphabets, as leaf nodes.

A generative grammar lays out the constructible set of well-formed propositions.

A finite set of propositions are distinguished as axioms. (Some would allow for an effectively enumerable set of axioms but without loss of generality we can assume a finite set.)

A finite set of computable structural relations between finite sets of propositions is defined which we call "inference rules".

All of the axioms are taken to be proved, by assumption.

Any proposition which can be reached from earlier proved propositions by a finite chain of inferences is also taken to be proved.

No other proposition is taken to be proved.

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

Starting from the above concept of math, something interesting arises.

In math, even as understood above, we can easily define uncountable sets (such as 2). We can also establish that some elements of such sets are "unconstructable".

Can terms of an uncountable set be used as terms (not necessarily "primitive terms", but terms) of a proposition?

We can allow members of ℕ as terms, what about 2?

On LtU, many have said (words to the effect) that some members of 2 can be used as terms but only, specifically, the constructable members. (I.e.: It is ok to represent some reals by their generating function.)

That's essentially the classic "constructivist" position.

The traditional objection to admitting unconstructable reals as terms in propositions can be loosely paraphrased as "Now you're just talking about how many angels can fit on the head of a pin!"

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

For the moment, let's suppose that we only allow computable reals to exist as terms in sentences. We allow them only in the form of a "generating" function.

Already, we have broken Goedel's proofs. They no longer work.

Not even Goedel's first theorem stands up to allowing computable reals as terms.

In this sense:

Goedel's proofs require the set of proofs to be computably enumerable.

The constructable reals are not computably enumerable (by diagonalization).

Q.E.D.

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

As an aside, in physics, quantum randomness seems to be a pretty real, irreducible phenomenon.

If we hypothesize that it is, then the following emerges:

A random bitstream of unbounded length may be constructed.

The set of all such possible bitstreams, of course, includes streams which are not computable. This is because given such a stream, and given a deterministic computation which allegedly computes the random bitstream, eventually (with probability 1) the random bitstream will prove the computation incorrect.

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

Uncontroversially: propositions can be drawn as finite expressions over finite sets.

Uncontroversially: propositions can allow computable reals as terms, and this is enough to already block Goedel's theorems, since we can no longer computable enumerate proofs.

Empirically, uncomputably random bitstreams of unbounded length appear to be constructable in the real world. Routable addresses of such physically realized bitstreams can certainly appear in data structures in computer programs and are in that sense on equal footing with any other possible term of a proposition's expression tree.

The main complaint about allowing these random bitstreams to be treated as reified, uncomputable reals is that they break Goedel's proofs but, in fact, we already broke those proofs when we let computable reals be used as terms.

Controversially

The bit about putting computable reals in terms looks wrong. If such a proposition (with a subterm encoded as a Turing machine representing a purported computable real) is proven, the proof will implicitly establish that the embedded Turing machine does indeed encode a computable real. The set of computable reals that appear in valid proofs will thus be an enumerable proper subset of all computable reals.

re controversially

Matt, that's a krazy-cooltm critique that I think is subtly wrong. To make a case (that I get your drift and that I think I can convince you it is wrong)... you argued:

If such a proposition (with a subterm encoded as a Turing machine representing a purported computable real) is proven, the proof will implicitly establish that the embedded Turing machine does indeed encode a computable real. The set of computable reals that appear in valid proofs will thus be an enumerable proper subset of all computable reals.

I think I can correctly paraphrase you this way (and correct me if I'm wrong):

Perhaps we can't uncontroversially admit "constructable reals" as terms in a theory because a theory's proofs are, by assumption, computationally enumerable. We assume a theory is is a proposition grammar over some finite alphabets, plus a finite number of propositions selected as axioms, plus a finite number of structural inference rules. The proofs are all the finite chains of inferences. These are obviously enumerable. Thus we can admit some constructable reals as terms in this theory, but only a computably countable subset of the constructable reals.

If we are talking about a foundation for mathematics in general, your reasoning had better not apply. Because...(for example)...

Given a theory that constructs some subset of constructable reals, a mathematician can rigorously construct a constructable real not available in that theory (by simple diagonalization, if nothing else).

What that tells us is that "constructable real" exists as a useful and rigorous class of terms, in "mathematics in general".

Repeating in different words:

Mathematicians robustly discuss the (not computably enumerable) "constructable reals", outside the context of any specific finitary formal system. (For example, We're doing it now. We're talking formalizably about the class of constructible reals in general, and are free to pick arbitrary imagined terms from it. If you're reading this: "You're soaking in it," as the old commercial used to say. We can rigorously reason about arbitrary terms from the constructable reals.)

The complete class of constructable reals is manifest as the space of potential creative acts by living practitioners of math. This is a class whose members people recognize when they see them.

If mathematics-in-general is to be formalized, it must admit terms that mathematicians discuss "between theories" (so to speak). A foundation should describe the class of available creative choices without pretending to rob them of creativity by enumerating tghem.

Describing the landscape

I agree with your paraphrase, but disagree with your reasoning that follows.

Mathematicians robustly discuss the (not computably enumerable) "constructable reals", outside the context of any specific finitary formal system.

There are two points of view one can take. One is that it is widely held that almost all of mathematics can be done inside set theory and that ZFC is an adequate formalization of set theory for this purpose. It is certainly possible, in ZFC, to reason about the set of all computable reals. In fact all of the arguments we're making here can be formalized in ZFC. So from this point of view, everything is fine with just a simple formal system.

The other point of view is to take a step back and ask which particular Turing machines can be proven to represent computable reals inside ZFC. A mathematician, believing in the soundness of ZFC, can then construct a new computable real by diagonalization that cannot be constructed inside of ZFC. This line of reasoning led Roger Penrose to argue in The Emperor's New Mind that mathematicians cannot be modeled as Turing machines and he went so far as to speculate that quantum mechanics might be crucial to the way mathematicians reason.

I think the situation is much more mundane: a human mathematician is simply unable to formalize his own mathematical thought process.

For example, let's take ZFC as system 0. By diagonalization, we can add a new axiom that gives us another computable real and call this system 1. Similarly we can obtain system 2, system 3, etc. A mathematician will have a flash of insight, though, and will quickly generalize to system n, for any natural n. He can then diagonalize over this entire pattern of all finite numbers and obtain system ω. Diagonalization of this system leads to system ω+1 and we can see that this pattern applies at every ordinal.

But a mathematician is unable to construct an arbitrary ordinal. We'll count 0, 1,2 ... ω, ω+1 ... 2ω, 2ω + 1,... ω*ω, ... polynomials of ω, ... The thing about counting ordinals is that we always feel like we're making progress, but the insights that are needed to get to a bigger class of ordinal get harder and harder.

So a mathematician will be able to produce a more powerful system for any system that we understand to be correct. But this will become more and more difficult as these systems rely on deeper and deeper insight for that correctness. There exists a sequence of systems approaching the limit of what a mathematician will understand, the union of which will be exactly what the mathematician could understand.

I suppose you could call this limit system "mathematics" and reason about it in the abstract, but I don't know what insights you might glean from doing so. It probably varies by mathematician and it seems mostly inaccessible to insight, by construction. This system will be enumerable, though, if you believe that people are ordinary machines and believe the Church-Turing thesis.

Uncountable many TMs

Take a countable number of TMs all generating different bitstreams. Construct a Cantor TM which runs every nth TM upto the nth bit and outputs the reversed bit.

Now I have established there are uncountably many TMs.

Where did I go wrong?

countable + 1 = countable

Where did I go wrong?

You started by assuming a countable set of TMs, and you showed the existence of one TM that you hadn't counted. But a countable infinity plus one is still a countable infinity.

Comment deleted

.
My argument here wasn't quite right. I don't see how to use diagonalization to generate the reals, so it was confused

You went wrong a few places

1) your Cantor TM contains all the other TMs therefor its length is infinite. The set of infinite length TMs is not countable.

2) you assumed that the set of outputs from your countable TMs is complete. But if there is a one to one correspondence between TMs and outputs then a countable set of TMs can't generate an uncountable set of reals - so there had to be holes.

But maybe the diagonalization argument is more slippery than it seems at first glance.

What if you applied the diagonalization argument, not to the set of reals but to the set of integers .. ie you prove that the list of integers isn't complete. Why is that less compelling as a proof that integers aren't countable?

Dunno

I am trying to make Lord's argument precise with TMs such that, hopefully, we'll know better where the argument is flawed (if so, of course).

I have some ideas about it but I think I'll just post it to stackexchange to see the response from a mathematician.

of why diagonalization doesn't apply to integers is that diagonalization constructs an infinite number that isn't in the list of integers, but the list of integers was pre-defined to not contain any infinite numbers.

Why constructable reals are not computably enumerable

The programming language TRIV is exactly like the the Scheme programming language in all respects except input and output.

TRIV has no provision for input. Programs only produce output.

TRIV output is limited to (any number, in any order) of the digits "0" and "1".

We define the class REAL_TRIV to be those TRIV programs which print an unbounded number of digits, and that always print additional digits after a finite amount of time.

It is possible to computably enumerate all TRIV programs. One can simply generate all strings from shortest to longest, and pick otu the subset of strings that are valid TRIV programs.

It is not possible to computably enumerate all of the REAL_TRIV programs because if you could do so, you could solve the halting problem for TRIV.

In that way, REAL_TRIV is countable since it is a subset of a countable set.

And REAL_TRIV is uncomputably countable because to count it would require solving the halting problem.

(This argument adapted from one by Andrej Bauer: http://mathoverflow.net/questions/30643/are-real-numbers-countable-in-constructive-mathematics)

It is not possible to

It is not possible to computably enumerate all of the REAL_TRIV programs because if you could do so, you could solve the halting problem for TRIV.

Actually, the way you've defined your programs, the halting problem for those programs is trivial: none of then ever halt. But even if you fix that definition, the unboundedness of the output is irrelevant to enumerating the machines, because the machines are not their output.

Funny

when I said the same thing to Thomas he accused me of not knowing the language of mathematics and not being rigorous...

Though Hewitt popped up at one point and agreed that his indeterminate actor (what is it called, Real[]...) is only one actor not an uncountable number of actors but he didn't acknowledge that this contradicted what he wrote before.

Sometimes I wonder if Thomas is a sockpuppet for Hewitt.

re Funny

Jokes on you Josh. To recognize members of REAL_TRIV you must be able to tell if a program diverges or does not diverge before printing more digits. That is an instance of the halting problem.

Sometimes I wonder if Thomas is a sockpuppet for Hewitt.

No, but we're both older and are more familiar with a lot of stuff that you probably know but don't always recognize when it comes around.

Real.[ ] a particular Actor: there are uncountable possibilities

Real.[ ] is a particular Actor; but there are uncountably many possibilities as to which one.

Uhm "which one"

How does it make any sense to associate an actor with it's output rather than its code?

- especially if you have random instructions.

The actor is its code, not what that code does in some random case.

That's a bit like saying that you have an infinite number of bombs because the shrapnel from one bomb can lie in many different ways after an explosion.

In an abstract sense Real.[] has only one possible output which is
{[a random digit], [a random digit],[a random digit], ... }

oh, c'mon now. this is silly: re Uhm "which one"

The actor is its code, not what that code does in some random case.

In unix, what is the difference between an executable and a process? Hmm? "Uhhmm?"

That's a bit like saying that you have an infinite number of bombs because the shrapnel from one bomb can lie in many different ways after an explosion.

:/ I have one piece of code 10 bytes long

and you say it's an uncountable infinity of actors...

You have managed to invent the world's most inefficient possible encoding, but you haven't added any information.

If I have one integer and encode it base pi so that it takes an infinite number of digits to encode that doesn't mean that I have an infinite amount of information, it just means that I suck at encoding.

Inefficient mappings do not make paradoxes

The number of programs/actors/thingamajigs defined by CODE in that uses A FINITE NUMBER OF SYMBOLS and is of A FINITE LENGTH is at most a countable infinity.

No one can argue with that. Period.

If you want to recast that countable infinity of thingamajigs as an uncountable number of results or anything else, then you've added nothing, you haven't increased the amount of thingamajigs, you've just mapped them inefficiently. The answer to the paradox is "stop mapping them badly"

If I map each integer to an uncountable infinity of things, that doesn't make integers uncountable, it just means that my mapping is so poor that it doesn't have the properties of the original sequence.

re inefficient mappings do not make paradoxes

Josh, you are bold faced and ALL CAPS arguing with uncontroversial, settled math, that you can read about elsewhere.

If you were taking a polite, inquisitive, and exhibiting-effort approach I'm sure it's at least likely people would want to help debug you but...

One more time:

You can enumerate programs, no problem, as you note. You can not computably enumerate programs that produce unbounded strings of 0s and 1s because if you could do so, then you would have in your hands a solution to the halting problem.

In my opinion, my side is uncontroversial, settled math

Let me add that programs with state are also countable.

Putting in an instruction that generates random events and pretending that the eternal future is a single event is allowing you to fool yourself about what is countable.

Also I note how pointedly you ignore the argument that is in bold text. Nice sidestep.

The definition of "countable" is not hard to understand, you know.

For any given list of reals, Real.[ ] might not be an element

For any given list of reals, Real.[ ] might not be an element, i.e., the reals are uncountable.

re It is not possible to

Not quite right, John:

Actually, the way you've defined your programs, the halting problem for those programs is trivial: none of then ever halt. But even if you fix that definition, the unboundedness of the output is irrelevant to enumerating the machines, because the machines are not their output.

The halting problem appears in REAL_TRIV context because we need to know if there is always a finite amount of time until the next digit to be printed. The question is whether or not the computation between printing digits halts.

The halting problem appears

The halting problem appears in REAL_TRIV context because we need to know if there is always a finite amount of time until the next digit to be printed. The question is whether or not the computation between printing digits halts.

Interesting. A strange case of misdirection. It honestly wouldn't have occurred to me you'd deliberately build an explicit requirement for eager decidability into your definition. The great advantage of enumeration lies in laziness; and besides, the title of your post suggested you were interested in the constructible reals, not incidental properties of the programs that generate them. Requiring your program to always produce another digit in finite time serves no apparent purpose other that to make it trivially impossible to enumerate all such programs (so trivially I'd have expected a much shorter demonstration of inenumerability if it were intentional).

Look, it's fine that you're represent constructible reals by programs that output sequences of binary digits. But if you remove the (frankly obstructionist) requirement that each such program be required to always output another digit, what have you lost? Nothing. You already weren't going to be able to decide whether or not two arbitrary programs represent the same real.

re the halting problem appears

Requiring your program to always produce another digit in finite time serves no apparent purpose other that to make it trivially impossible to enumerate all such programs .

What you have said here is that you want to argue about the constructable reals while displaying ignorance of what the term means. Really basic level ignorance. Like you have made no visible effort to learn the term at all. It is not a hard concept. There are tons of materials on-line from which you may get a clue. It is a very basic concept that doesn't require any advanced math. Young kids who make an effort easily get the concept. I'm not sure what excuse you might have other than comment forums bring out the worst in lots of people.

If you are sincere, you should stop commenting for a while and try to learn more because you are saying some pretty ignorant things.

If you are not, then now we have identified an actual troll.

I have no interest in

I have no interest in arguing, and never have; I detest it. I perceive that when I try to help you hone your understanding, you interpret it as arguing. Therefore I'll stop trying to help.

The best way to hone my understanding is to make your point directly, not try to play psychological games.

All subsets of countable sets are countable so the constructable reals are countable.

A set is computably enumerable if a program can generate all of its elements such that every element will be produced as output in finite time.

The constructable reals are countable but not computably enumerable.

This is not something new I just made up. Its not controversial.

A strange case of misdirection. It honestly wouldn't have occurred to me you'd deliberately build an explicit requirement for eager decidability into your definition.

"misdirection" is an accusation, to which you add the insinuation of "deliberately" and "your definition" which is why I replied harshly.

If you honestly can not fathom why decidability is built-in to the definition of "constructable real" then you don't know what the words mean.

Remember that this whole topic arises under the question of Goedel's arguments which require that we be able to effectively enumerate proofs.

Uncountable random bitstreams

Uncountable random bitstreams do not exist. You either require infinite space (for an infinite qbit machine) or infinite time (to repeatedly get output from a finite qbit machine).

Until you can experimentally construct one, what you have is theoretical physics (and incorrect in my opinion). The fact is you can define equations in mathematics that have nothing to do with reality and call it theoretical physics, and get good predictions most of the time. Relativity came from the assumption "what would spacetime look like if the speed of light were constant". Initially this was just a mathematical exercise to understand how such a hypothetical system would behave. This hypothetical mathematical system can be imagined independently of the true nature of the universe. Only by experimentally measuring the speed of light are we able to verify that locally the universe does behave like this, but we are not sure whether it approximates reality at cosmic scales and timescales. So although you can imagine and mathematically model a universe in which infinite bitstreams can exist,that does not mean they exist in our universe. Einstein puts it better:

As far as the laws of mathematics refer to reality, they are not certain, and as far as they are certain, they do not refer to reality.

To dismiss this argument as sophistry is to demonstrate a profound misunderstanding of what physics is.

re Uncountable random bitstreams do not exist.

Uncountable random bitstreams do not exist.

Yes, but mathematicians can still rigoursly reason about arbitrary members of the class of potential random bitstreams that physical construction can choose from. A foundation for math-in-general should permit that.

Second order statement

And those mathematicians would be reasoning in second order logic, and those statements can be assigned finite Gödel numbers.

Types categorically axiomatize uncountably many reals

Using types, the Dedekind axioms categorically axiomatize uncountably many reals.

It is irrelevant that there is a Gödel number for the Peano/Dedekind type-checked string for the axioms that categorically defined real numbers.

Categories typically realise many axiomatic uncountabilities.

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

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

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

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

Wrong categorical

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

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

Categorical

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

Constructable Reals

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

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

re I disagree that the constructable Reals are uncountable.

The constructable reals are countable.

They are uncomputably countable.

Go figure.

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

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

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

Human Brain and Finite Godel Numbers.

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

BTW Hewitt: another typo and a rough spot in DL paper

In the DL paper footnote where the constructions for types are given, the construction for Terms of some type σ is given twice. (The first time it is footnoted so probably the second one is the typo.)

Also, Terms is nowhere else used or explained which is slightly rough. A sentence, perhaps.

overview of the DL paper

AFAICT,

CDL gives a theory of types with primitive types Boolean, ℕ Sentence, Proposition, Proof, and Theory. From previously constructed types, new types can be constructed for disjoint unions, functions, and so forth.

Axioms of construction are given for ℕ

A strong axiom of induction is given for ℕ and as a result it has but one model.

Axioms of construction for typed sets are given but there is no set-specific strong axiom of induction. Sets are established by a characteristic function.

(Therefore, btw, I was wrong, earlier, when I said in a nearby thread that DL lacked a universal set of for ℕ but I think I was still correct that it lacks a universal set for Sets◁ℕ▷. We don't have a provably universal powerset of the naturals because we have no categorical induction axiom for Set◁ℕ▷, We do have a universal set for ℕ itself because the categorical induction axiom for naturals lets us prove that all naturals are found in the set given by the characteristic function that always returns true. Hope I have that right now.)

The paper doesn't give (or I missed) axioms for Boolean but these are not too difficult to come up with. :-)

Rules of construction are given for typed expressions and sentences, which can be abstracted to form propositions. No axiom of induction is given for these.

A conservative but natural set of rules of inference are given.

Here is one big point:

Unlike what people are used to:

CDL does not give a strong axiom of induction for types. The set of types is open-ended. You can extend DL with new types.

CDL does not define any particular construction rules for functions, families, etc. You can invent new ways to introduce objects of this kind.

CDL is rigorously open-ended/incomplete.

One crude reason you can not enumerate the proofs of CDL is because CDL does not give you enough specification of proofs to be able to do that! (At the same time, you can enumerate all of the natural numbers in CDL, because the axioms for natural numbers give you enough to do that.)

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

The "propositions of CDL are uncountable" because it is possible to define theories within CDL in which, for example, we have a kind of constructive way to choose a truly random real number.

If you find uncountable propositions unpalatable, stick to some other sub-theory of CDL.

CDL is not the kind of "foundation" wherein we have specified, once and for all, all the axioms we need.

CDL is the kind of "foundation" wherein we have axioms atop which we expect to add additional axioms and definitions.

Direct Logic intention: a rigorous mathematical foundation of CS

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

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

The core of CDL is

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

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

no model re the core of cdl

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

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

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

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

Models

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

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

I think you're being bamboozled.

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

not a multiverse re models

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

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

DL is simultaneously three things:

1. DL is the metatheory of DL.

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

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

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

In some sub-theories, proofs may be enumerable.

In other sub-theories, not necessarily.

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

re bamboozled

BTW:

I think you're being bamboozled.

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

One model per type

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

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

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

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

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

re one model per type

AFAIK:

Some subtheories have no models because of definitional incompleteness.

Some subtheories have multiple models.

Some subtheories have a unique model up to isomorphism.

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

Such a subltle, slick theory.

This is really subtle and hella slick. For example, there is no provably universal set of sets of naturals because the only way to conduct such a proof would be in terms of the strong axiom of induction over naturals. Yet if you could do that, you would have to first enumerate the subsets of the naturals.

Sets◅ℕ▻ is a type, but *not* a set in Mathematics

Thanks Thomas!

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

Separate theories can be provided for more speculative extensions.

Finite and Infinite

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

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

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

re How would you model integer rings in DL?

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

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

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

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

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

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

Also, after defining ℤ, you could prove:

Theorem: GroupSpecification[Integers, +, 0]

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



Forall g?

I thought DL did not have a universal quantifier?

quantifier elimination in DL re Forall g?

(Thanks for this question.)

I thought DL did not have a universal quantifier?

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


Propositions can be formed according to this rule:

If σ1,σ2:Type, x1:σ1 and x2:σ2, then
x1:x2:Proposition

The univeral quantiifer is a short-hand:

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

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

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

In the context of set theory:

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

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

For example, the group theory axioms begin:

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

which could be (less expressively but equivalently) written:

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


Modeling machine integers

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

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

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

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

closure axioms (re How would you model integer rings in DL?)

I think I missed one axiom here:

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

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

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



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

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


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

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

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