PeteOlcott wrote: ↑Fri Aug 16, 2019 7:06 pm
I applaud your effort suggesting an excellent way for me to make my ideas perfectly concrete.
Your suggestion has spawned my creative process for replicating the functionality of Prolog as
applied to higher order logic defined entirely as stipulated relations between finite strings.
I showed how to define axioms in my prior reply to this message. By using the syntax of Prolog
I can define Facts (axioms) and Rules (rules of inference) as stipulated relations between
finite strings. I have not yet figured out how to adapt this syntax to specify higher order logic.
Since Prolog already defines FOL as stipulated relations between finite strings, the idea that
formal systems can be defined this way is already fully elaborated for FOL in Prolog.
Everything you have said above boils down to expressive power.
What I am warning you against is the Turing tarpit
Beware of the Turing tar-pit in which everything is possible but nothing of interest is easy.
In theory, everything you can do in C++ or Prolog - you can do in Brainfuck also.
The reason WHY you don't is very, very important. Human usability.
A language with rich vocabulary is very concise.
A language with poor vocabulary is very verbose.
A programming language like Mathematica has an exceptional vocabulary.
You can express incredibly complex ideas from broad domains of knowledge in a just a few lines of code.
A programming language like Brain fuck is the exact opposite of that.
Both Mathematica and Brainfuck are Turing-complete.
This exact property (expressivity) applies to logic also. FOL is atrocious! There is a reason Prolog is dead.
Worse - you are trying to retro-fit high-order logic on top of FOL. You are doing it backwards! Why?
Just start with a language that has been designed as a high-order logic from the start.
I urge you, advise you and encourage you to learn a high-level programming language. Start at the highest level of abstraction you can work your way to.
Python, Ruby, TypeScript, Julia - it doesn't matter. Just pick any language that uses dynamic typing!
Something that does not require the rigour and strictness of static typing like C++
Something that is almost as natural, expressive as intuitive as speaking English!
You are so used to having type safety in your programming languages that you are trying to shoehorn human knowledge into a strongly normalising type-safe system.
It's perfectionism at its worst. It's unnecessary. It's pure masochism. It's outright inhumane.
You remind me of me in my 20s. Trying to adapt the world to my brilliant design, rather than adapting my design to the world.