Second-Order Monadic Modal Logic with Axioms as Rules

Second-order purely universal axioms can be reduced to arithmetical inference rules that allow a proof analysis. We apply this axioms-as-rules method to a classical second-order monadic modal logic ( SOMLc SOML c ) with explicit predicative comprehension for a countable language. This logic is shown, through a reduction procedure, to be a conservative extension of first-order modal logic extended with rules ( FOMLc FOML c ). Termination of the reduction procedure requires an explicit vector expression measure that corresponds to induction on natural numbers. As a consequence the consistency of a second-order arithmetic with predicative comprehension follows assuming transfinite induction up to ε ₀ ε 0 on elementary recursive predicates EA-TI(ε ₀) E A - T I ( ε 0 ) . The second part implements the method for Gödel’s ontological proof. Two standard variants, Scott’s version and Anderson’s emendation, of the argument are considered. The ontological argument proving the necessary existence of a godlike individual, formally ∃ x. G(x) □ ∃ x . G ( x ) , uses classical indirect reasoning to prove the possible existence of a godlike individual. By the reduction of SOMLc SOML c extended with ontological rules to FOMLc FOML c , and by a formula transformation that replaces G with falsity, intuitionistic underivability of ∃ x. G(x) □ ∃ x . G ( x ) is shown for the predicative monadic modal logic. The proof of reduction reduces derivability of ∃ x. G(x) □ ∃ x . G ( x ) in SOMLc SOML c to derivability of an inconsistency in propositional modal logic. Because the second-order underivability result requires the reduction to first-order provability, the proof is relative, and assumes EA-TI(ε ₀) E A - T I ( ε 0 ) .