/true-fol-formulas-over-r

This haskell program will eventually generate any true first order logic formula over the set of all real numbers, ℝ. Hopefully. I'm not a mathematician. Credit goes to: Philip Lukert, Felix Mujkanovic.

Primary LanguageHaskellMIT LicenseMIT

True first order logic formulas over ℝ

This is a haskell program. It's neither a particularly nice nor beautiful one. Still, it will eventually generate any true first order logic formula over the set of all real numbers, ℝ. Hopefully. I'm not a mathematician.

Actually, the list is not really complete, since the terms are lacking functions like abs or sin, and even vital real constants like π. The following term elements are supported however:

  • The constants 0 and 1
  • Addition, and by extension all constants in ℕ
  • The additive inverse, and by extension all constants in ℤ
  • Multiplication
  • The multiplicative inverse, and by extension all constants in ℚ

Notably, constants in ℝ are not supported. Also note that obeying to my continous quest to eliminate as many parentheses as possible, the additive inverse doesn't get them, so terms representations like ---1⋅-1 are, while unusual and maybe a bit confusing at first, possible.

Usage

You can simply run the program like this:

runhaskell TrueFOLFormulasOverR.hs
1       ∀x. ⟨x+0⟩=x
2       ∀x. ∀y. ⟨x+y⟩=⟨y+x⟩
3       ∀x. ∀y. ∀z. ⟨x+⟨y+z⟩⟩=⟨⟨x+y⟩+z⟩
4       ∀x. ¬∀y. ¬⟨x+y⟩=0
5       ∀x. ⟨x⋅1⟩=x
6       ∀x. ∀y. ⟨x⋅y⟩=⟨y⋅x⟩
7       ∀x. ∀y. ∀z. ⟨x⋅⟨y⋅z⟩⟩=⟨⟨x⋅y⟩⋅z⟩
8       ∀x. (¬x=0 → ¬∀y. ¬⟨x⋅y⟩=1)
9       ¬1=0
10      ∀x. ∀y. ∀z. ⟨x⋅⟨y+z⟩⟩=⟨⟨x⋅y⟩+⟨x⋅z⟩⟩
...

Try it for yourself!

When you open the program file in GHCi or even import the file into your own haskell program, you will have some additional options:

  • printTerms prints an infinite list of all possible terms with respect to the rules above (e.g., x-⟨y⋅⟨1+1⟩⟩), ordered by increasing length.
  • printPropositions prints an infinite list of all combinations of two terms using either the operator = or <, ordered by increasing length. This list contains both true and false propositions.
  • printFormulas prints an infinite list of all first order logic formulas, ordered by increasing length. This list contains both true and false formulas.
  • printLaxiomInsts prints an infinite list of all true first order logic formulas you can obtain by putting all possible formulas into the basic axioms of first order logic. Note that the resulting list of formulas is no longer strictly ordered by length. However, the list is still kind of ordered.
  • printStaticAxioms prints the finite and quite short list containing all the basic "static" axioms of ℝ.
  • printTrueFormulas prints the final infinite list of all true formulas. It is generated by taking the axioms of ℝ, slowly adding laxiomInsts and repeatedly applying modus ponens and generalization over time. Calling this function results in the same behavior as calling main.

If you don't want to look at a pretty-printed list, but instead need the raw list object of any of the lists mentioned above, just take away the print. For example, trueFormulas will yield the raw inifinite list containing all true formulas.