Who knows lambda calculus?

[PeteOlcott]

(1) To express all of the functionality of any formal system.

How do you express Turing-completeness in a Type-2 grammar?

I don't see any case where the conventional notion of a formal system requires Turing completeness.

[PeteOlcott]

(2) What true thing about integers cannot be expressed in a type-2 language?

A declarative query which answers the question: "How many facts does this formal system know?"

Some of these facts are algorithmically compressed as algorithms, thus the list is finite and countable.

[PeteOlcott]

It seems to me that HOL can express any true thing, and HOL can be expressed
as a type-2 language.

Type-2 languages cannot do reflection

But you are really fucking confused about what it is that you are trying to do. Lambda calculus is the formalisation of a Turing machine.
Lambda calculus can RECOGNIZE "all formal grammars" (whatever their syntax)

Reflection is not required and Lambda Calculus was a mere first guess of a sufficient formal system with minimal syntax.

I am shooting for the minimal specification of the most generic notion of a formal system and
probably do not need to expressive power of type-0.

[Skepdick]

Reflection is not required

By whom and for what purpose? I USE reflection when I construct formal systems (a.k.a program) every damn day.

As far as I am concerned if it can't DO reflection it's not a formal system. In fact - it's such a strong criterion that as far as I am concerned Mathematics is not a formal system.

I am shooting for the minimal specification of the most generic notion of a formal system and
probably do not need to expressive power of type-0.

You are trying to derive a 'generic notion' of a formal system ,while you are trying to ignore the generic notion of expressive power.

You are confused about the fundamental purpose of formal systems. If I don't want to EXPRESS any formalisms - I don't need a formal system.

[PeteOlcott]

Reflection is not required

By whom and for what purpose? I USE reflection when I construct formal systems (a.k.a program) every damn day.

As far as I am concerned if it can't DO reflection it's not a formal system. In fact - it's such a strong criterion that as far as I am concerned Mathematics is not a formal system.

I am shooting for the minimal specification of the most generic notion of a formal system and
probably do not need to expressive power of type-0.

You are trying to derive a 'generic notion' of a formal system ,while you are trying to ignore the generic notion of expressive power.

You are confused about the fundamental purpose of formal systems. If I don't want to EXPRESS any formalisms - I don't need a formal system.

To define the "=" relation between finite strings of numeric digits for the +(S1, S2) function requires an algorithm.
Except for the unlimited tape, "C" seems to be Turing Complete. So what level language is "C" ?

[Skepdick]

To define the "=" relation between finite strings of numeric digits for the +(S1, S2) function requires an algorithm.

Why do you want to define the "=" relation? There are plenty of algorithms possible where "=" is not required.

Except for the unlimited tape, "C" seems to be Turing Complete. So what level language is "C" ?

So is Brainfuck. They are both Type 0. In theory. In practice, they are qualitatively different.

[Skepdick]

Some of these facts are algorithmically compressed as algorithms, thus the list is finite and countable.

You clearly didn't understand this the last time I punched you in the face with this point.

In practice - how long would it take you to count the finite set of all integers?
In practice - how many times can you re-count the finite set of all integers?

Is counting to 100 once the same as counting to 50 twice?

[PeteOlcott]

To define the "=" relation between finite strings of numeric digits for the +(S1, S2) function requires an algorithm.

Why do you want to define the "=" relation? There are plenty of algorithms possible where "=" is not required.

Everyone understands that arithmetic of natural numbers concurrently defines
true and provable. We only know that 2 + 3 = 5 because the axioms prove this.

I am trying to make a generic notion of formal systems that is simple enough
that everyone understands that true and provable are always concurrently
defined for every formal system.

[Skepdick]

Everyone understands that arithmetic of natural numbers concurrently defines
true and provable. We only know that 2 + 3 = 5 because the axioms prove this.

I can trivially misunderstand this for the sake of contrarianism. But I am not in the mood.

Formal systems are just tools. Humans use tools to accomplish arbitrary tasks. What is the task at hand?

I am trying to make a generic notion of formal systems that is simple enough
that everyone understands that true and provable are always concurrently
defined for every formal system.

Why do you want to blur the lines between truth and provability when they are clearly distinct notions?

There are true statements which can be made about formal system by way of their behaviour in the world that cannot be proven within the formal system itself.

You are failing to distinguish denotational from operational semantics.

[vegetariantaxidermy]

When geeks argue

[PeteOlcott]

Everyone understands that arithmetic of natural numbers concurrently defines
true and provable. We only know that 2 + 3 = 5 because the axioms prove this.

I can trivially misunderstand this for the sake of contrarianism. But I am not in the mood.

Why do you want to blur the lines between truth and provability when they are clearly distinct notions?

Until we have a perfectly correct understanding of natural language semantics it will be impossible
to automatically populate a knowledge ontology and thus create strong AI.

One of the key aspects of a correct understanding of semantics that is missing is
the only way that we know that formalized semantics is true is that it is provable.

A sequence of sound inference beginning with true premises derives true conclusions.
It seems somewhat insane that anyone would have ever thought differently.

https://plato.stanford.edu/entries/goed ... pleteness/
The first incompleteness theorem states that in any consistent formal system F within
which a certain amount of arithmetic can be carried out, there are statements of the
language of F which can neither be proved nor disproved in F.

[Skepdick]

Until we have a perfectly correct understanding of natural language semantics it will be impossible
to automatically populate a knowledge ontology

Well, first you have to learn to walk before you can run. You don't even understand formal semantics.

and thus create strong AI.

Your conception of AI is still based on the old "expert systems" approach. It's a dead end for all the reasons well understood. But it's specifically a dead-end because of the frame problem.

Elephants don't play chess: https://en.wikipedia.org/wiki/Nouvelle_AI

One of the key aspects of a correct understanding of semantics that is missing is
the only way that we know that formalized semantics is true is that it is provable.

That is only denotational semantics, not operational semantics.

You cannot prove the statement "This program is feee of errors".

A sequence of sound inference beginning with true premises derives true conclusions.

That is not true in a non-deterministic universe. Deductive reasoning can lead to false conclusions with entropy.

https://en.wikipedia.org/wiki/Inductive_reasoning

Deductive certainty is impossible in non-axiomatic systems such as reality, leaving inductive reasoning as the primary route to (probabilistic) knowledge of such systems

[PeteOlcott]

A sequence of sound inference beginning with true premises derives true conclusions.

That is not true in a non-deterministic universe. Deductive reasoning can lead to false conclusions with entropy.

None-the-less it proves that formal systems are not incomplete or inconsistent, math has no entropy.

[Skepdick]

None-the-less it proves that formal systems are not incomplete or inconsistent, math has no entropy.

It proves no such thing. Mathematicians are entropy to maths. Interpretation is Operational Semantics.

And... https://en.wikipedia.org/wiki/Entropy_(computing)

(non)determinism is just another operational semantic.

[PeteOlcott]

None-the-less it proves that formal systems are not incomplete or inconsistent, math has no entropy.

It proves no such thing. Mathematicians are entropy to maths. Interpretation is Operational Semantics.

And denotationally, the entire field of stochastics/probability theory is about entropy.

None of that has anything to do with sound deductive inference.
Sound deductive inference requires truth preserving operations to be applied to true premises deriving truth.
Any formal system diverging from this model is incorrect.