Prover9's Simplification Explained Away

This note discusses P. Oppenheimer and E. Zalta's ‘A Computationally-Discovered Simplification of the Ontological Argument’ [this journal, 2011]. I try to explain why the simplification presented there was successful and comment on the technical aspects of the method they applied.     

Adaptation to Reversal of Retinal Feedback of Eyemovements

Both optical and hybrid-computer methods were devised to reverse the visual feedback which the eye gets of its own movements. Optical reversal by a contact lens device caused persisting, unstable, skittered, blurred vision, to which the subject made no effective adaptation. Using a hybrid analog-digital-analog computer, eyemovement-retinal feedback was reversed by yoking oscilloscope targets to the transduced electrical signals of ocular movements and reversing the sign of input-output control of the computer system. Vision with such computer-reversed feedback from ocular movements duplicated the experiences with the contact-lens method. Practice over five sessions of 50 trials indicated that three Ss showed no significant improvement in eye-tracking accuracy with the reversed vision. Perception of direction in vision and the basic signal processes of vision were thus found to be dependent on built-in direction specificity of eyemovement-retinal feedback interactions which also govern dynamic specialization and control of pursuit, saccadic, and fixation movements.     

Exploring the Non-objectified Character of Dao in the Laozi: A Modem Articulation

This article focuses on the interpretation of heng dao 恆 道 (sometimes translated as "the constant dao") and its fundamental character in the Laozi.It argues against the prevailing interpretation of dao as an unchanging metaphysical substance or reality,and maintains that the fundamental feature of heng dao is both dynamic and eternal.Heng dao is beyond language because of its dynamic character,but the Laozi nevertheless strives to express it in three aspects:1) its flexibility and adaptability as represented in the metaphor of water;2) its movement of reversal and return;3) and in its existential significance as a guide for life.Heng dao can be called the non-objectified dao,which produces law,principle,rule,method,and so on.Looked at in this way,the dynamic character of heng dao can be called non-objective.     

Identical Twins,Deduction Theorems,and Pattern Functions: Exploring the Implicative BCSK Fragment of S5

We recapitulate (Section 1) some basic details of the system of implicative BCSK logic, which has two primitive binary implicational connectives, and which can be viewed as a certain fragment of the modal logic S5. From this modal perspective we review (Section 2) some results according to which the pure sublogic in either of these connectives (i.e., each considered without the other) is an exact replica of the material implication fragment of classical propositional logic. In Sections 3 and 5 we show that for the pure logic of one of these implicational connectives two – in general distinct – consequence relations (global and local) definable in the Kripke semantics for modal logic turn out to coincide, though this is not so for the pure logic of the other connective, and that there is an intimate relation between formulas constructed by means of the former connective and the local consequence relation. (Corollary 5.8. This, as we show in an Appendix, is connected to the fact that the ‘propositional operations’ associated with both of our implicational connectives are close to being what R. Quackenbush has called pattern functions.) Between these discussions Section 4 examines some of the replacement-of-equivalents properties of the two connectives, relative to these consequence relations, and Section 6 closes with some observations about the metaphor of identical twins as applied to such pairs of connectives.     

Sequent Calculi for Some Strict Implication Logics

We introduce various sequent systems for propositional logicshaving strict implication, and prove the completeness theoremsand the finite model properties of these systems.The cut-eliminationtheorems or the (modified) subformula properties are provedsemantically.     

Connection Tableau Calculi with Disjunctive Constraints

Automated theorem proving amounts to solving search problems in usually tremendous search spaces. A lot of research therefore focuses on search space reductions. Our approach reduces the search space which arises when using so-called connection tableau calculi for first-order automated theorem proving. It uses disjunctive constraints over first-order equations to compress certain parts of this search space. We present the basics of our constrained-connection-tableau calculi, a constraint extension of connection tableau calculi, and deal with the efficient handling of constraints during the search process. The new techniques are integrated into the automated connection tableau prover Setheo.     

A Note on Goodman's Theorem

Goodman's theorem states that intuitionistic arithmetic in all finite types plus full choice, HA + AC, is conservative over first-order intuitionistic arithmetic HA. We show that this result does not extend to various subsystems of HA, HA with restricted induction.     

Causality assessment in epidemiology

Epidemiology relies upon a broad interpretation of determinism. This paper discusses analogies with the evolution of the concept of cause in physics, and analyzes the classical nine criteria proposed by Sir Austin Bradford Hill for causal assessment. Such criteria fall into the categories of enumerative induction, eliminative induction, deduction and analogy. All of these four categories are necessary for causal assessment and there is no natural hierarchy among them, although a deductive analysis of the study design is preliminary to any assessment.     

Naming and Diagonalization, from Cantor to Godel to Kleene

We trace self-reference phenomena to the possibility of namingfunctions by names that belong to the domain over which thefunctions are defined. A naming system is a structure of theform (D, type( ),{ }), where D is a non-empty set; for everya D, which is a name of a k-ary function, {a}: D^k D is thefunction named by a, and type(a) is the type of a, which tellsus if a is a name and, if it is, the arity of the named function.Under quite general conditions we get a fixed point theorem,whose special cases include the fixed point theorem underlyingGödel's proof, Kleene's recursion theorem and many othertheorems of this nature, including the solution to simultaneousfixed point equations. Partial functions are accommodated byincluding "undefined" values; we investigate different systemsarising out of different ways of dealing with them. Many-sortednaming systems are suggested as a natural approach to generalcomputatability with many data types over arbitrary structures.The first part of the paper is a historical reconstruction ofthe way Gödel probably derived his proof from Cantor'sdiagonalization, through the semantic version of Richard. Theincompleteness proof–including the fixed point construction–resultfrom a natural line of thought, thereby dispelling the appearanceof a "magic trick". The analysis goes on to show how Kleene'srecursion theorem is obtained along the same lines.