A first-order conditional probability logic.

*(English)*Zbl 1251.03030In this paper the logic LFOCP is introduced. This logic allows the formalization of “the conditional probability of \(\varphi\) given \(\psi\) is at least \(c\)”, where \(\varphi\), \(\psi\) are first-order formulae.

In the introduction the authors discuss related work, set out their agenda and summarize their main results.

In the two following sections, syntax and semantics for LFOCP are described. The semantics is given in a possible-world formulation.

Section four contains an infinitary axiom system containing the axioms for classical propositional logic and five inference rules, which are briefly discussed.

Section five is the technical main part of the paper, which contains proofs of soundness and completeness of LFOCP.

The authors go on to show that a probabilistic formula \(\alpha\) based on a decidable part of first-order logic is decidable.

In the seventh and final section the authors give an example of the expressive power of LFOCP.

A related paper, co-authored by the second author, may also be of interest [A. Ilić-Stepić, Z. Ognjanović, N. Ikodiniović and A. Perović, Math. Log. Q. 58, No. 4–5, 263–280 (2012; Zbl 1251.03027)].

In the introduction the authors discuss related work, set out their agenda and summarize their main results.

In the two following sections, syntax and semantics for LFOCP are described. The semantics is given in a possible-world formulation.

Section four contains an infinitary axiom system containing the axioms for classical propositional logic and five inference rules, which are briefly discussed.

Section five is the technical main part of the paper, which contains proofs of soundness and completeness of LFOCP.

The authors go on to show that a probabilistic formula \(\alpha\) based on a decidable part of first-order logic is decidable.

In the seventh and final section the authors give an example of the expressive power of LFOCP.

A related paper, co-authored by the second author, may also be of interest [A. Ilić-Stepić, Z. Ognjanović, N. Ikodiniović and A. Perović, Math. Log. Q. 58, No. 4–5, 263–280 (2012; Zbl 1251.03027)].

Reviewer: Jürgen Landes (Canterbury)