Информационная система по формальным теориям

Теория QTV

Теория QTV – классическая логика предикатов первого порядка в языке LQPr с алфавитом AQPr и классом ППТ VT. .

Схемы аксиом QTV:

Схемы аксиом классической логики высказываний;
xA(x) A(t), если не одна переменная из терма t не оказывается связанной в результате такой подстановки;
x(A B) (A xB), если A не содержит свободных вхождений x;
A xA.

Правила вывода:

Правило modus ponens (правило отделения): ((AB), A) => B.

Определение класса ППТ VT:
1) {x₁, y₁, z₁, x₂, y₂, z₂, ..., x_n, y_n, z_n, ...}VT;
2) {a₁, b₁, c₁, d₁, a₂, b₂, c₂, d₂, ..., a_n, b_n, c_n, d_n, ...}VT;
3) (t₁, t₂, ..., t_n є VT) => (fⁿ(t₁, t₂, ..., t_n) є VT).

Определение класса ППФ LQPr:
1) (t₁, t₂, ... t_n є VST) => (P(t₁, t₂, ... t_n) є LQPr);
2) (A, B є LQPr) => (¬A, (A&B), (AB), (AB), (AB), xA(x), xA(x) є LQPr).