Philosophy Now Forum

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?

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.

Skepdick wrote: ↑Fri Sep 13, 2019 8:49 am 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 !!!

PeteOlcott wrote: ↑Fri Sep 13, 2019 4:36 pm 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.

PeteOlcott wrote: ↑Fri Sep 13, 2019 4:36 pm 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.

Skepdick wrote: ↑Fri Sep 13, 2019 8:49 am You are trying to define the syntax of Lambda calculus (Type 0 grammar) using BNF (Type 2 grammar).

Skepdick wrote: ↑Fri Sep 13, 2019 4:49 pm

PeteOlcott wrote: ↑Fri Sep 13, 2019 4:36 pm 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.

PeteOlcott wrote: ↑Fri Sep 13, 2019 5:09 pm 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.

Skepdick wrote: ↑Fri Sep 13, 2019 5:11 pm

PeteOlcott wrote: ↑Fri Sep 13, 2019 5:09 pm 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!

Skepdick wrote: ↑Fri Sep 13, 2019 8:49 am You are trying to define the syntax of Lambda calculus (Type 0 grammar) using BNF (Type 2 grammar).

Skepdick wrote: ↑Fri Sep 13, 2019 4:49 pm 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.

PeteOlcott wrote: ↑Fri Sep 13, 2019 5:22 pm 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.

PeteOlcott wrote: ↑Fri Sep 13, 2019 2:04 am 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?

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

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.

PeteOlcott wrote: ↑Fri Sep 13, 2019 6:42 pm 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?

Skepdick wrote: ↑Fri Sep 13, 2019 6:56 pm

PeteOlcott wrote: ↑Fri Sep 13, 2019 6:42 pm 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.

PeteOlcott wrote: ↑Fri Sep 13, 2019 7:08 pm 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.

Skepdick wrote: ↑Fri Sep 13, 2019 7:12 pm

PeteOlcott wrote: ↑Fri Sep 13, 2019 7:08 pm 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.

PeteOlcott wrote: ↑Fri Sep 13, 2019 7:19 pm (1) To express all of the functionality of any formal system.

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

PeteOlcott wrote: ↑Fri Sep 13, 2019 7:19 pm (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?"

PeteOlcott wrote: ↑Fri Sep 13, 2019 7:19 pm 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)