Syntaks

[17.12.2023] [Nørderier/Teori]

• Intro
• Udvidelse af udsangslogik
• Syntaks
• Semantik
• Naturlig Deduktion
• Ækvivalenser

Altså grammatik for prædikatlogik. Lad antallet af argumenter et prædikat eller en funktion tager, være betegnet aritet. Først og fremmest har vi termer:

• Variable er termer. Dvs. \( x,y, \dots \) er termer.
• En hvilken som helst konstant, \( c \), er en term.
• Hvis \( t_1, t_2, \dots , t_n \) er termer og \( f \) en funktion med aritet \( n \geq 1 \), så er \( f(t_1, t_2, \dots , t_n) \) en term

Intet andet er en term.

For formler har vi:

• Hvis \( P \) er et prædikat med aritet \( n \geq 1 \), og hvis \( t_1, t_2, \dots, t_n \) er termer, så er \( P(t_1, t_2, \dots , t_n) \) en formel.
• Hvis \( \phi \) er en formel, så er \( \neg \phi \) en formel.
• Hvis \( \phi, \psi \) er formler, er \( \phi \star \psi \), for \( \star \in \{ \land, \lor, \rightarrow \} \) en formel.
• Hvis \( \phi \) er en formel, så er \( (\phi) \) en formel.
• Hvis \( \phi \) er en formel og \( x \) en variabel, så er \( \forall x . \phi \) og \( \exists x . \phi \) en formel.

Husk at vi har at et prædikat af aritet 0 er et udsagnsatom. Det inkluderer vi som formel. Intet andet er en formel. Argumenterne til prædikaterne er termer. Derfor kalder vi denne logik for førsteordens. Havde vi haft at et prædikat kunne tage prædikater som argumenter, var logikken af højere orden. Vi har at \( \forall, \exists \) binder lige så stærkt som \( \neg \). Resten er som ved udsagnslogik. Altså:

• \( \neg,\forall x, \exists x \) binder tættest.
• \( \land,\lor \) binder næst tættest.
• \( \rightarrow \) binder mindst tæt samt er højre-associativ.

Frie og bundne variable

En grammatik som denne giver anledning til et syntakstræ. Måske får jeg taget mig sammen til at tegne et på et tidspunkt. En variable, \( x \), er bunden, hvis der dukker en kvantor op som forældre når man vader op gennem træet. Ellers er x fri. Vi kalder alt under en kvantor i træet for inden for kvantorens scope (i mangel på et dansk ord). Vi kan angive dette med []. Feks. givet $$ \forall x (P(x) \land Q(x)) \lor \neg P(x) $$ Her har vi $$ [\forall x . P(x) \land Q(x) ] $$ bundet til scopet under kvantoren. Hvorimod formlen $$ \neg P(x) $$ er fri.

Substitution

Givet en formel \( \phi \) samt en term \( t \) og en variabel \( x \) har vi at \( \phi[t / x] \) er formlen hvor vi substituerer alle frie forekomster af \( x \) med \( t \).

Substitutionsmarkøren \( \phi[t / x] \) er ikke en del af logikken eller grammatikken.

Substitution sker i syntakstræet.

Fri for \( x \) i \( \phi \)

Der kan opstå problemer. Lad feks. \( t = f(y,y) \) en term. Siden \( t \) er en term, kan den ikke indeholde en kvantor. Altså er \( y \) fri. OK. Vi laver følgende manøvre \( (\exists y. P(x) \lor P(y))[t/x] \). Og vi får: $$ (\exists y . P(f(y,y)) \lor P(y)) $$ og så er \( y \) i \( f(y,y) \) jo bundet af eksistenskvantoren. Derfor indfører vi følgende definition:

Definition

Lad \( t \) være en term. Lad \( x \) en variabel. Lad \( \phi \) en formel. Vi siger \( t \) er fri for \( x \) i \( \phi \) hvis ingen variabel \( y \) i \( t \) bliver bundet efter \( x \) er blevet substitueret med \( t \) i \( \phi \). Altså efter \( \phi[t/x] \).

Index Del