Who knows lambda calculus?

[PeteOlcott]

I am trying to validate the simplest possibly notion of a formal system as relations between finite strings.
I know that Lambda Calculus has the expressive power of a Turing Machine:

<λexp> ::= < var >
| λ . <λexp>
| ( <λexp> <λexp> )

I was thinking that it might be possible so somehow convert the functionality of
lambda calculus into syntax that is closer to predicate logic by defining named
functions that take finite string arguments and return finite string values.

Does anyone here have any ideas on this?

[Skepdick]

You are trying to define the syntax of Lambda calculus (Type 0 grammar) using BNF (Type 2 grammar).

There are so many metaphors that come to mind here - I don't even know which one to insult you with.

[PeteOlcott]

You are trying to define the syntax of Lambda calculus (Type 0 grammar) using BNF (Type 2 grammar).

There are so many metaphors that come to mind here - I don't even know which one to insult you with.

It is already common knowledge across very many academic sources that the above BNF is correct.

Ha, Ha I got You !!! Your bias is showing !!!

[Skepdick]

It is already common knowledge across very many academic sources that the above BNF is correct.

Idiot. In what grammar was BNF's 'correctness' proven?

Did BNF prove itself correct? No.

BNF cannot SAY anything about its own correctness. yacc/bcc are implemented in C.

Ha, Ha I got You !!! Your bias is showing !!!

I guess I don't need to use metaphors. I can simply tell you that you are a moron.

In fact. I wish I had a grammar sufficiently powerful to express the level of stupid I think you are, but such grammar does not exist.

So I shall leave it unsaid.

[PeteOlcott]

You are trying to define the syntax of Lambda calculus (Type 0 grammar) using BNF (Type 2 grammar).

It is already common knowledge across very many academic sources that the above BNF is correct.

Ha, Ha I got You !!! Your bias is showing !!!

It's also common knowledge that BNF is not powerful enough to express Type 1 and Type 0 semantics,

You lost track of the distinction between syntax and semantics.

[Skepdick]

You lost track of the distinction between syntax and semantics.

I didn't lose track. You don't understand the distinction.

You cannot validate any 'correctness' property of BNF in BNF. Syntactic or semantic.

That is why you IMPLEMENT the BNF parser in C.

[PeteOlcott]

You lost track of the distinction between syntax and semantics.

I didn't lose track. You don't understand the distinction.

Now you are a liar, going back and changing what
you said and claiming that you never said it!

You are trying to define the syntax of Lambda calculus (Type 0 grammar) using BNF (Type 2 grammar).

It's also common knowledge that BNF is not powerful enough to express Type 1 and Type 0 semantics,

The syntax of lambda calculus can be defined in BNF.

[Skepdick]

The syntax of lambda calculus can be defined in BNF.

Sigh.

https://www.cs.ccu.edu.tw/~naiwei/cs5605/YaccBison.html

Any grammar expressed in BNF is a context-free grammar.

I know that Lambda Calculus has the expressive power of a Turing Machine:

So Is Lambda calculus Type 0 or Type 2? Neither? Both? You are too stupid to tell?

[Skepdick]

More?

Not all context-free languages can be handled by Yacc/Bison, only those that are LALR(1)
https://en.wikipedia.org/wiki/LALR_parser

Do you know what the (1) means? 1 token look-ahead.
Do you know what a token is? https://en.wikipedia.org/wiki/Type%E2%8 ... istinction

[PeteOlcott]

We wasted all this time over trivialities.

The point was to define at the most abstract level the syntax and semantics the most generic notion of a formal system from which every possible formal system could be defined.

We can coalesce the notions of functions and predicates into a function that may return Boolean or some other value.

We can coalesce the notion of infix logical connectives as postfix Boolean functions named for the infix operator.

Can you see where this is going? Can you add to this?
For example: Could quantifiers be Boolean functions named for the quantifier?

∀x ∈ Natural_Numbers ∃y ∈ Natural_Numbers (y > x)

∀(x, ∈(x, Natural_Numbers))
∃(y, ∈(y, Natural_Numbers))
>(x, y)

I am currently unsure how to connect those functions together.

[Skepdick]

The point was to define at the most abstract level the syntax and semantics the most generic notion of a formal system from which every possible formal system could be defined.

https://en.wikipedia.org/wiki/Chomsky_h ... 0_grammars

Type-0 grammars include all formal grammars.

You know what ALL means, right?

[PeteOlcott]

The point was to define at the most abstract level the syntax and semantics the most generic notion of a formal system from which every possible formal system could be defined.

https://en.wikipedia.org/wiki/Chomsky_h ... 0_grammars

Type-0 grammars include all formal grammars.

You know what ALL means, right?

The notion of a formal system would be met by a type-0 language.
The notion of a formal system may not require a type-0 language a type-2 language may be sufficiently expressive.

[Skepdick]

The notion of a formal system may not require a type-0 language a type-2 language may be sufficiently expressive.

That is not a complete sentence. Sufficiently expressive to... do what ? The notion of a formal system may (or may not) require to... do what?

Obviously a type-2 language is NOT sufficiently expressive to say true things about the integers.
Obviously a more powerful system is required to say things about the integers.

[PeteOlcott]

The notion of a formal system may not require a type-0 language a type-2 language may be sufficiently expressive.

That is not a complete sentence. Sufficiently expressive to...... do what ?

Obviously a type-2 language is NOT sufficiently expressive to say true things about the integers.

(1) To express all of the functionality of any formal system.
(2) What true thing about integers cannot be expressed in a type-2 language?

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

[Skepdick]

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

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

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

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)