06

@mester - Here. What?

Szekvent módszer szintaxisa

• \(\Gamma, \Delta:\) Véges formulahalmazok (véges, nem rendezett formulasorozatok)
• \(A,\dots,B\) formulák
• \((\Gamma,\Delta)\) pár: szekvent jelölése \(\Gamma \rightarrow \Delta\)

Akár \(\Gamma\), akár \(\Delta\) formulahalmaz lehet üres

• Ha \(\Gamma\) üres, a \(\emptyset \rightarrow \Delta\) helyett \(\red{\rightarrow \Delta}\)
• Ha \(\Delta\) üres, a \(\Gamma \rightarrow \Delta\) helyett \(\red{\rightarrow \Gamma}\)
• Mindkét formulahalmaz lehet üres szekvent: \(\red{\rightarrow}\)
• Ha \(\Gamma\) = {\(A_1, A_2, \dots, A_n\)} és \(\Delta\) = {\(B_1, B_2, \dots, B_n\)} véges nem rendezett formulasorozatok és \(A, B\) ítéletlogikai formulák, akkor \(\red{A,\Gamma \rightarrow \Delta B }\)-t írunk, ami az \(A_1, A_2, \dots, A_n \rightarrow B_1, B_2, \dots, B_mB\quad\) szekventet jelenti

Elsőrendben a szintaxis egyértelműen ugyanaz

Szekvent jelentése

Szemantika alapján

• \(B_I(\rightarrow) = h\)
• \(B_I(\rightarrow B) = B_I(B)\)
• \(B_I(A \rightarrow) = B_I(\neg A)\)
• \(B_I(A \rightarrow B) = B_I(A \supset B)\)
• \(B_I(A1, A2 \rightarrow B1, B2) = B_I(A1 \land A2 \supset B1 \lor B2)\)

G kalkulus szabályai

Axiómaséma

Levezetési szabályok