Ana Martins

We review five recent works [1, 2, 9, 15, 16] which present natural deduction systems for linear logic, or for fragments of that logic, and introduce a new single-conclusion natural deduction system for first-order classical linear logic named NDLL. Moreover, we demonstrate the equivalence between the NDLL system and Girard's linear sequent calculus, and prove the weak normalization theorem and its usual companion: the subformula principle for normal deductions in NDLL.NDLL gives rules for the whole of linear logic, including new rules for “Par” “Why not” . We also investigate these new rules and their implications to the normalization procedure through a proof-theoretical perspective

The notion of the least fixed point of an operator is widely applied in computer science as, for instance, in the context of query languages for relational databases. Some extensions of first-order classical logic with fixed point operators, as the least fixed point logic, were proposed to deal with problems related to the expressivity of FOL. LFP captures the complexity class PTIME over the class of finite ordered structures. The descriptive characterization of computational classes is a central issue within finite model theory. Trahtenbrot's theorem states that validity over finite models is not recursively enumerable, that is, completeness fails over finite models. This result is based on an underlying assumption that any deductive system is of finite nature. However, we can relax such assumption as done in the scope of proof theory for arithmetic. Motivated by Gödel incompleteness theorems, proof theory for arithmetic offer an example of a true mathematically meaningful principle non-derivable in first-order arithmetic. One way of presenting this proof is based on a definition of a proof system with an infinitary rule, the ω-rule, that establishes the consistency of first-order arithmetic through a proof-theoretical perspective. Inspired in this rule, here we will propose an infinitary natural deduction system, and a sequent calculus version, for FOL and LFP restricted to finite models, FOLfin and LFPfin, respectively, we will prove soundness and completeness for them and also normal form theorems for them. With this infinitary deductive system for LFPfin, we aim to present a proof theory for a logic traditionally investigated within the scope of FMT. It opens up an alternative way of proving results already obtained within FMT and also new ones through a proof-theoretical perspective.

We investigate some logics which use the concept of minimal models in their definition. Minimal objects are widely used in Logic and Computer Science. They are applied in the context of Inductive Definitions, Logic Programming and Artificial Intelligence. An example of logic which uses this concept is the MIN logic due to van Benthem [20]. He shows that MIN is equivalent to the Least Fixed Point logic in expressive power. In [6], we extended MIN to the MIN Logic and proved it is equivalent to second-order logic in expressive power. Here, we exhibit a fragment of MIN, the MINΔ logic, which is more expressive than LFP, less expressive than MIN and closed under boolean connectives and first-order quantification. In order to do this, in the Section 2, we prove that the Downward Löwenheim-Skolem Theorem holds for arbitrary countable sets of LFP-formulas by showing that every infinite structure has a countable LFP-substructure. The method may be used to generalize this theorem to any set of LFP-formulas. We also analyse the expressive power of the Nested Abnormality Theories of Lifschitz, another formalism based on minimal models used in Artificial Intelligence, and we demonstrate that for each second-order theory Γ there is a NAT which is a conservative extension of Γ. We give a translation from second-order sentences into such NATs which is linear in the size of the sentence in prenex normal form. Finally, we establish a hierarchy of expressiveness of these logics that deal with the concept of minimal models

Documento recente do Ministério da Educação aponta para a construção da identidade desse curso como sendo etapa final que compõe a educação básica e sinalizando a busca constante pela superação da dualidade considerada histórica entre formação geral e profissionalização. Entretanto, o mesmo documento reconhece que essa contradição ainda se faz presente na realidade educacional brasileira e, em alguns momentos, afirma a necessidade de uma educação integrada e em outros reforça a profissionalização aos mais pobres que não podem esperar o Ensino Superior para ingressar no mercado de trabalho. O texto a seguir busca analisar a fragmentação na identidade do atual Ensino Médio remontando a suas bases históricas, a do partir dos textos de Nunes e Souza que acabam por reforçar a conclusão de que os dilemas em torno da questão “formação geral e formação profissional” ainda não foram totalmente superados, apesar dos apontamentos dos documentos legais

Natural deduction systems for classical, intuitionistic and modal logics were deeply investigated by Prawitz [D. Prawitz, Natural Deduction: A Proof-theoretical Study, in: Stockholm Studies in Philosophy, vol. 3, Almqvist and Wiksell, Stockholm, 1965. Reprinted at: Dover Publications, Dover Books on Mathematics, 2006] from a proof-theoretical perspective. Prawitz proved weak normalization for classical logic only for a language without logical or, there exists and with a restricted application of reduction ad absurdum. Reduction steps related to logical or, there exists and classical negation bring about many problems solved only rather recently. For classical S5 modal logic, Prawitz defined a normalizable system, but for a language without logical or, there exists, ◊ and, for a propositional language without ◊, Medeiros [M.da P.N. Medeiros, A new S4 classical modal logic in natural deduction, Journal of Symbolic Logic 71 799–809] presented a normalizable system for classical S4. We can mention many cut-free Gentzen systems for S4, S5 and K45/K45D, some normalizable natural deduction systems for intuitionistic modal logics and one more for full classical S4, but not for full classical S5. Here our focus is on the definition of a classical and normalizable natural deduction system for S5, taking not only □ and ◊ as primitive symbols, but also all connectives and quantifiers, including classical negation, disjunction and the existential quantifier. The normalization procedure is based on the strategy proposed by Massi [C.D.B. Massi, Provas de normalizaçaõ para a lógica clássica, Ph.D. Thesis, Departamento de Filosofia, UNICAMP, Campinas, 1990] and Pereira and Massi [L.C. Pereira, C.D.B. Massi, Normalização para a lógica clássica, in: O que nos faz pensar, Cadernos de Filosofia da PUC-RJ, vol. 2, 1990, pp. 49–53] for first-order classical logic to cope with the combined use of classical negation, disjunction and the existential quantifier. Here we extend such results to deal with □ and ◊ too. The elimination rule for ◊ uses the notions of connection and of essentially modal formulas already proposed by Prawitz for the introduction of □. Beyond weak normalization, we also prove the subformula property for full S5

We investigate expressiveness and definability issues with respect to minimal models, particularly in the scope of Circumscription. First, we give a proof of the failure of the Löwenheim-Skolem Theorem for Circumscription. Then we show that, if the class of P; Z-minimal models of a first-order sentence is Δ-elementary, then it is elementary. That is, whenever the circumscription of a first-order sentence is equivalent to a first-order theory, then it is equivalent to a finitely axiomatizable one. This means that classes of models of circumscribed theories are either elementary or not Δ-elementary. Finally, using the previous result, we prove that, whenever a relation Pi is defined in the class of P; Z-minimal models of a first-order sentence Φ and whenever such class of P; Z-minimal models is Δ-elementary, then there is an explicit definition ψ for Pi such that the class of P; Z-minimal models of Φ is the class of models of Φ ∧ ψ. In order words, the circumscription of P in Φ with Z varied can be replaced by Φ plus this explicit definition ψ for Pi.