Proof systems for infinite behaviours (Q1193598): Difference between revisions

The paper suggests several generalizations of testing to \(\omega\)- behaviours of communicating processes, analyses the logical complexity of the testing equivalences, and establishes on that basis a connection with proof systems. Section 2 supplies infinitary tests with infinitary results for the equality of linear \(\omega\)-behaviours in pure CCS. Section 3 contains an introduction to \(\omega\)-logic and recalls the strong connection between \(\Pi^ 1_ 1\) and the \(\omega\)-rule. Section 4 establishes a mutual reduction between \(\Pi^ 1_ 2\) formulas of arithmetic and formulas \(p\approx q\), where \(\approx\) is the equivalence over CCS programs induced by tests defined in section 2; it is concluded therefrom that complete systems of \(\omega\)-proofs for \(\approx\) cannot exist. Sections 5 and 6 investigate the logical complexity of two alternative equivalences based on families of finitary resp. infinitary tests with binary results, namely the equivalence of De Nicola and Hennessy resp. the equivalence of ``indiscernibility''. It is shown that indiscernibility is not \(\Pi^ 1_ 1\) and has therefore no complete system of recursive \(\omega\)-proofs, in contrast to De Nicola and Hennessy's equivalence. Section 7 contains an elementary introduction to Girard's work in \(\beta\)-logic showing the existence of complete systems of recursive proofs for indiscernibility and for \(\approx\).