한 논리학자가 꿈나라로 갔다. 꿈나라에서는 다음과 같은 방법으로 '공리'를 정의한다.

임의의 논리식 α_1, ..., α_n, β에 대하여, 문자열

α_1, ..., α_n / β.

은 "임의의 변수배정이 주어졌을 때, α_1, ..., α_n가 모두 참이면 β도 참이다."는 뜻하는 공리이다.

대신 꿈나라에서는 한정사와 결합자를 이용하여 논리식을 만들지 않는다.

공리계는 공리계의 집합이고, 공리계로부터 참임을 유도할 수 없는 논리식의 진리값은 그 변수 배정에서 거짓으로 정의된다.

한편 대상영역 대신 타입이란 객체가 있고, 타입은 생성자들의 집합이다. 생성자는 0항 이상의 함수로 봐도 되는 것 같다.

값은 생성자들과 값의 결합이며, 항은 값과 생성자들의 결합이고, 식은 술어와 항의 결합이다.

다음은 자연수와 더하기를 정의하는 코드이다.

1 Nat ::= zero() | succ(Nat). - 타입 Nat 정의. zero는 Nat의 0항 생성자, succ은 Nat의 1항 생성자이다.

2 Plus(Nat, Nat, Nat). - 3항 술어 Plus 선언.

3 / Plus(n, zero(), n). - 임의의 n에 대하여 식 Plus(n, zero(), n)은 항상 참이다.

4 Plus(i, j, k) / Plus(i, succ(j), succ(k)). - 임의의 i, j, k에 대하여 Plus(i, j, k)가 참이면 Plus(i, succ(j), succ(k))도 참이다.

이 공리계에서 모든 변수 배정에 대하여 식 Plus(zero(), x, x)이 참임을 알 수 있다.

이때 임의의 변수 배정에 대하여 Φ가 참이면 ψ가 거짓이고, Φ가 거짓이면 ψ가 참인

두 논리식 φ, ψ에 관한 공리계가 존재하는가?

제가 만든 자작 문제입니다. 답은 저도 몰라요.