We prove constructively that for any propositional formula in Conjunctive Normal Form, we can either find a satisfying assignment of true and false to its variables, or a refutation of showing that it is unsatisfiable. This refutation is a resolution proof of ¬. From the formalization of our proof in Coq, we extract Robinson’s famous resolution algorithm as a Haskell program correct by construction. The account is an example of the genre of highly readable formalized mathematics.

We constructively prove completeness for intuitionistic first-order logic, iFOL, showing that a formula is provable in iFOL if and only if it is uniformly valid in intuitionistic evidence semantics as defined in intuitionistic type theory extended with an intersection operator.Our completeness proof provides an effective procedure that converts any uniform evidence into a formal iFOL proof. Uniform evidence can involve arbitrary concepts from type theory such as ordinals, topological structures, algebras and so forth. We have implemented that procedure in the (...) Nuprl proof assistant.Our result demonstrates the value of uniform validity as a semantic notion for studying logical theories, and it provides new techniques for showing that formulas are not intuitionistically provable. Here we demonstrate its value for minimal and intuitionistic first-order logic. (shrink)

Types now play an essential role in computer science; their ascent originates from Principia Mathematica. Type checking and type inference algorithms are used to prevent semantic errors in programs, and type theories are the native language of several major interactive theorem provers. Some of these trace key features back to Principia.

We examine metonymy at psycho- and neurolinguistic levels, seeking to adjudicate between two possible processing implementations. We compare highly conventionalized systematic metonymy to lesser-conventionalized circumstantial metonymy. Whereas these two metonymy types differ in terms of contextual demands, they each reveal a similar dependency between the named and intended conceptual entities. We reason that if each metonymy yields a distinct processing time course and substantially non-overlapping preferential localization pattern, it would not only support a two-mechanism view but would suggest that conventionalization (...) acts as a linguistic categorizer. By contrast, a similar behavior in time course and localization would support a one-mechanism view and the inference that conventionalization acts instead as a modulator of contextual felicitousness, and that differences in interpretation introduced by conventionalization are of degree, not of kind. Results from three paradigms: self-paced reading, event-related potentials, and functional magnetic resonance imaging, reveal the following: no main effect by condition for either metonymy type immediately after the metonymy trigger, and a main effect for only the Circumstantial metonymy one word post-trigger ; a N400 effect across metonymy types and a late positivity for Circumstantial metonymy ; and a highly overlapping activation connecting the left ventrolateral prefrontal cortex and the left dorsolateral prefrontal cortex. Altogether, the pattern observed does not reach the threshold required to justify a two-mechanism system. Instead, the pattern is more naturally understood as resulting from the implementation of a generalized referential dependency mechanism, modulated by degree of context dependence/conventionalization, thus supporting architectures of language whereby “lexical” and “pragmatic” meaning relations are encoded along a cline of contextual underspecification. (shrink)