View source for Formula (FOL)

{{Stub page|grade=A|msg=Created so I wouldn't have to sift through notes or scour PDFs. It requires more references and some fleshing out to link to other pages. But will suffice for now}}
==Definition==
The logical formulas of a [[FOL]] are (like {{link|terms|FOL}}) defined [[inductive definition|inductively]] by the following 5 rules{{rMLFFISWL}}:
# If {{M|t_1}} and {{M|t_2}} are {{link|terms|FOL}} then {{M|t_1\doteq t_2}} is a formula
# If {{M|t_1,\ldots,t_m}} are {{link|terms|FOL}} and {{M|P}} is an {{M|m}}-[[airty|ary]] {{link|predicate symbol|FOL}} then {{M|Pt_1\cdots t_m}} is a formula
# If {{M|A}} is a formula, then {{M|(\neg A)}} is a formula
# If {{M|A}} and {{M|B}} are formulas then:
#* {{M|(A\wedge B)}}, {{M|(A\vee B)}}, {{M|(A\rightarrow B)}} and {{M|(A\leftrightarrow B)}} are all formulas too
#** Note, as mentioned on the [[FOL]] page, we can define some of these {{link|logical connective symbols|FOL}} in terms of the others. Keep that in mind here
# If {{M|A}} is a formula and {{M|x}} is a {{link|variable symbol|FOL}} then both:
#* {{M|\forall xA}} and {{M|\exists xA}} are formulas
#** Again from the [[FOL]] page recall that we can define {{M|\forall }} using {{M|\exists}} and {{M|\exists}} using {{M|\forall}}
We have been rather lax in how we use brackets here. In practice we shall use them whenever they help readability, and also discard them whenever it helps, for example:
# {{M|\exists x(x\doteq y)}} is easier to read than {{M|\exists xx\doteq y}}
# {{M|A\vee B\vee C\vee D}} is easier to read than {{M|(((A\vee B)\vee C)\vee D)}}
If we fixed (1) by changing rule 5 to {{M|\forall x(A)}} and {{M|\exists x(A)}} then we'd have lots of things that look like:
* {{M|\exists x((\ldots \rightarrow \ldots)) }}
So just be comfortable that we ''could'' write everything out totally unambiguously using lots of brackets without having to address the issue of parsing.
===[[BNF]] Definition===
I don't like this (as it is written now), it needs cleaning up. But using<ref name="MLFFISWL"/> we get:
* {{C|1=Formula ::= Term {{M|\doteq}} Term {{!}} PREDICATE (Term)<sub>{{n|times}}</sub> {{!}} {{M|\neg}} Formula {{!}} Formula ({{M|\wedge}}{{!}}{{M|\vee}}{{!}}{{M|\rightarrow}}{{!}}{{M|\leftrightarrow}}) Formula {{!}} ({{M|\forall}}{{!}}{{M|\exists}}) VARIABLE Formula}}
{{Todo|Clean this up, write a grammar that is "correct". For example there should be brackets on everything between the {{M|\vert}}s. This reads like "term followed by {{M|\doteq}} followed by (Term or PREDICATE ....) }}
==Terminology==
* {{Anchor|atomic formula}}Any formula given by rules {{M|1}} or {{M|2}} is called an {{link|atomic formula|FOL}}.
* {{Anchor|composite formula}}Any other formula is called a {{link|composite formula|FOL}}
==See next==
* {{link|Free variables|FOL}}
* {{link|Term substitution|FOL}}
* {{link|Formula substitution|FOL}}
* {{link|Model|FOL}}
* {{link|Assignment|FOL}}
* {{link|Structure|FOL}}
==References==
<references/>
{{Formal logic navbox|plain}}
{{Definition|Formal Logic}}