Structuralist Logic: Implications, Inferences, and Consequences

On a structuralist account of logic, the logical operators, as well as modal operators are defined by the specific ways that they interact with respect to implication. As a consequence, the same logical operator (conjunction, negation etc.) can appear to be very different with a variation in the implication relation of a structure. We illustrate this idea by showing that certain operators that are usually regarded as extra-logical concepts (Tarskian algebraic operations on theories, mereological sum, products and negates of individuals, intuitionistic operations on mathematical problems, epistemic operations on certain belief states) are simply the logical operators that are deployed in different implication structures. That makes certain logical notions more omnipresent than one would think. Mathematics Subject Classification (2000): Primary 03B22; Secondary 03B20, 03B42, 03B60     

A Finite Hilbert-Style Axiomatization of the Implication-Less Fragment of the Intuitionistic Propositional Calculus

In this paper we obtain a finite Hilbert-style axiomatization of the implicationless fragment of the intuitionistic propositional calculus. As a consequence we obtain finite axiomatizations of all structural closure operators on the algebra of {–}-formulas containing this fragment. Mathematics Subject Classification: 03B20, 03B22, 06D15.     

Provably recursive functions of constructive and relatively constructive theories

In this paper we prove conservation theorems for theories of classical first-order arithmetic over their intuitionistic version. We also prove generalized conservation results for intuitionistic theories when certain weak forms of the principle of excluded middle are added to them. Members of two families of subsystems of Heyting arithmetic and Buss-Harnik’s theories of intuitionistic bounded arithmetic are the intuitionistic theories we consider. For the first group, we use a method described by Leivant based on the negative translation combined with a variant of Friedman’s translation. For the second group, we use Avigad’s forcing method.     

From Fibring to Cryptofibring. A Solution to the Collapsing Problem

The semantic collapse problem is perhaps the main difficulty associated to the very powerful mechanism for combining logics known as fibring. In this paper we propose cryptofibred semantics as a generalization of fibred semantics, and show that it provides a solution to the collapsing problem. In particular, given that the collapsing problem is a special case of failure of conservativeness, we formulate and prove a sufficient condition for cryptofibring to yield a conservative extension of the logics being combined. For illustration, we revisit the example of combining intuitionistic and classical propositional logics. Mathematics Subject Classification (2000): 03B22 (03B35, 03G25, 03G30)     

Typical ambiguity and elementary equivalence

A sentence of the usual language of set theory is said to be stratified if it is obtained by “erasing” type indices in a sentence of the language of Russell's Simple Theory of Types. In this paper we give an alternative presentation of a proof the ambiguity theorem stating that any provable stratified sentence has a stratified proof. To this end, we introduce a new set of ambiguity axioms, inspired by Fraïssé's characterization of elementary equivalence; these axioms can be naturally used to give different proofs of the ambiguity theorem (semantic or syntactic, classical or intuitionistic). MSC: 03B15, 03F50, 03F55.     

Cut-Elimination Theorem for the Logic of Constant Domains

The logic CD is an intermediate logic (stronger than intuitionistic logic and weaker than classical logic) which exactly corresponds to the Kripke models with constant domains. It is known that the logic CD has a Gentzen-type formulation called LD (which is same as LK except that (→) and (?–) rules are replaced by the corresponding intuitionistic rules) and that the cut-elimination theorem does not hold for LD . In this paper we present a modification of LD and prove the cut-elimination theorem for it. Moreover we prove a “weak” version of cut-elimination theorem for LD , saying that all “cuts” except some special forms can be eliminated from a proof in LD . From these cut-elimination theorems we obtain some corollaries on syntactical properties of CD : fragments collapsing into intuitionistic logic. Harrop disjunction and existence properties, and a fact on the number of logical symbols in the axiom of CD . Mathematics Subject Classification : 03B55. 03F05.     

Ternary Operations as Primitive Notions for Constructive Plane Geometry IV

In this paper we provide a quantifier-free constructive axiomatization for Euclidean planes in a first-order language with only ternary operation symbols and three constant symbols (to be interpreted as ‘points’). We also determine the algorithmic theories of some ‘naturally occurring’ plane geometries. Mathematics Subject Classification: 03F65, 51M05, 51M15, 03B30.     

The eskolemization of universal quantifiers

This paper is a sequel to the papers Baaz and Iemhoff (2006, 2009) [4], [6] in which an alternative skolemization method called eskolemization was introduced that, when restricted to strong existential quantifiers, is sound and complete for constructive theories. In this paper we extend the method to universal quantifiers and show that for theories satisfying the witness property it is sound and complete for all formulas. We obtain a Herbrand theorem from this, and apply the method to the intuitionistic theory of equality and the intuitionistic theory of monadic predicates.     

An Intuitionistic Axiomatisation of Real Closed Fields

We give an intuitionistic axiomatisation of real closed fields which has the constructive reals as a model. The main result is that this axiomatisation together with just the decidability of the order relation gives the classical theory of real closed fields. To establish this we rely on the quantifier elimination theorem for real closed fields due to Tarski, and a conservation theorem of classical logic over intuitionistic logic for geometric theories.     

On Overspill Principles and Axiom Schemes for Bounded Formulas

We study the theories I?_n, L?_n and overspill principles for ?_n formulas. We show that IE_n ? L?_n ? I?_n, but we do not know if I?_n L?_n. We introduce a new scheme, the growth scheme Crγ, and we prove that L?_n ? Cr?_n? I?_n. Also, we analyse the utility of bounded collection axioms for the study of the above theories. Mathematics Subject Classification: 03F30, 03H15.     

The eskolemization of universal quantifiers

This paper is a sequel to the papers Baaz and Iemhoff (2006, 2009) [4] and [6] in which an alternative skolemization method called eskolemization was introduced that, when restricted to strong existential quantifiers, is sound and complete for constructive theories. In this paper we extend the method to universal quantifiers and show that for theories satisfying the witness property it is sound and complete for all formulas. We obtain a Herbrand theorem from this, and apply the method to the intuitionistic theory of equality and the intuitionistic theory of monadic predicates.     

Comparing material and structural set theories

We study elementary theories of well-pointed toposes and pretoposes, regarded as category-theoretic or “structural” set theories in the spirit of Lawvere's “Elementary Theory of the Category of Sets”. We consider weak intuitionistic and predicative theories of pretoposes, and we also propose category-theoretic versions of stronger axioms such as unbounded separation, replacement, and collection. Finally, we compare all of these theories formally to traditional membership-based or “material” set theories, using a version of the classical construction based on internal well-founded relations.     

An Application of Logic to Combinatorial Geometry: How Many Tetrahedra are Equidecomposable with a Cube?

It is known (see Rapp [9]) that elementary geometry with the additional quantifier “there exist uncountably many” is decidable. We show that this decidability helps in solving the following problem from combinatorial geometry: does there exist an uncountable family of pairwise non-congruent tetrahedra that are n-equidecomposable with a cube? Mathematics Subject Classification: 03B25, 03C80, 51M04, 52B05, 52B10.     

A dominance intuitionistic fuzzy-rough set approach and its applications

Although the rough set and intuitionistic fuzzy set both capture the same notion, imprecision, studies on the combination of these two theories are rare. Rule extraction is an important task in a type of decision systems where condition attributes are taken as intuitionistic fuzzy values and those of decision attribute are crisp ones. To address this issue, this paper makes a contribution of the following aspects. First, a ranking method is introduced to construct the neighborhood of every object that is determined by intuitionistic fuzzy values of condition attributes. Moreover, an original notion, dominance intuitionistic fuzzy decision tables (DIFDT), is proposed in this paper. Second, a lower/upper approximation set of an object and crisp classes that are confirmed by decision attributes is ascertained by comparing the relation between them. Third, making use of the discernibility matrix and discernibility function, a lower and upper approximation reduction and rule extraction algorithm is devised to acquire knowledge from existing dominance intuitionistic fuzzy decision tables. Finally, the presented model and algorithms are applied to audit risk judgment on information system security auditing risk judgement for CISA, candidate global supplier selection in a manufacturing company, and cars classification.     

Categories with families and first-order logic with dependent sorts

First-order logic with dependent sorts, such as Makkai's first-order logic with dependent sorts (FOLDS), or Aczel's and Belo's dependently typed (intuitionistic) first-order logic (DFOL), may be regarded as logic enriched dependent type theories. Categories with families (cwfs) is an established semantical structure for dependent type theories, such as Martin-Löf type theory. We introduce in this article a notion of hyperdoctrine over a cwf, and show how FOLDS and DFOL fit in this semantical framework. A soundness and completeness theorem is proved for DFOL. The semantics is functorial in the sense of Lawvere, and uses a dependent version of the Lindenbaum-Tarski algebra for a DFOL theory. Agreement with standard first-order semantics is established. Applications of DFOL to constructive mathematics and categorical foundations are given. A key feature is a local propositions-as-types principle.     

直觉主义类型论中π和Σ规则的研究

本文研究直觉主义类型论中π和Σ规则，对于类型（πｘ∈Ａ）Ｂ（ｘ），我们给出新的消去和相等规则使新规则的式样与其他类型的规则相同，然而不使用高阶交元和常元，我们证明新规则等价于旧规则，对于类型（Σｘ∈Ａ）Ｂ（ｘ），我们利用投影运算给出新规则，而且证明它们等价于旧规则。     

Intuitionistic completeness of first-order logic

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.     

直觉模糊模型检测在工程决策上的应用

将直觉模糊Kripke结构扩展到加权直觉模糊Kripke结构,将直觉模糊计算树逻辑诱导到加权直觉模糊计算树逻辑;研究在此之上的直觉模糊期望测度和多属性工程决策问题。用加权直觉模糊Kripke结构的权值自然地刻画了工程问题中的成本和收益,直觉模糊测度量化工程进展的不确定性,用加权直觉模糊计算树逻辑描述不确定性工程属性约束。给出了基于直觉模糊模型检测的多属性工程寻优算法,并讨论了算法的复杂度。     

Decidability of ∀*∀-Sentences in Membership Theories

The problem is addressed of establishing the satisfiability of prenex formulas involving a single universal quantifier, in diversified axiomatic set theories. A rather general decision method for solving this problem is illustrated through the treatment of membership theories of increasing strength, ending with a subtheory of Zermelo-Fraenkel which is already complete with respect to the ?*? class of sentences. NP-hardness and NP-completeness results concerning the problems under study are achieved and a technique for restricting the universal quantifier is presented. Mathematics Subject Classification: 03B25, 03E30.