Admissible rule

In logic, a rule of inference is admissible in a formal system if the set of theorems of the system does not change when that rule is added to the existing rules of the system. In other words, every formula that can be derived using that rule is already derivable without that rule, so, in a sense, it is redundant. The concept of an admissible rule was introduced by Paul Lorenzen (1955). Admissibility has been systematically studied only in the case of structural (i.e. substitution-closed) rules in propositional non-classical logics, which we will describe next. Let a set of basic propositional connectives be fixed (for instance, in the case of superintuitionistic logics, or in the case of monomodal logics). Well-formed formulas are built freely using these connectives from a countably infinite set of propositional variables p0, p1, .... A substitution σ is a function from formulas to formulas that commutes with applications of the connectives, i.e., for every connective f, and formulas A1, ... , An. (We may also apply substitutions to sets Γ of formulas, making σΓ = {σA: A ∈ Γ}.) A Tarski-style consequence relation is a relation between sets of formulas, and formulas, such that for all formulas A, B, and sets of formulas Γ, Δ. A consequence relation such that for all substitutions σ is called structural. (Note that the term "structural" as used here and below is unrelated to the notion of structural rules in sequent calculi.) A structural consequence relation is called a propositional logic. A formula A is a theorem of a logic if . For example, we identify a superintuitionistic logic L with its standard consequence relation generated by modus ponens and axioms, and we identify a normal modal logic with its global consequence relation generated by modus ponens, necessitation, and (as axioms) the theorems of the logic. A structural inference rule (or just rule for short) is given by a pair (Γ, B), usually written as where Γ = {A1, ... , An} is a finite set of formulas, and B is a formula. An instance of the rule is for a substitution σ.

About this result

This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

Related publications (13)

Related units (2)

Related concepts (9)

Related courses (1)

Related lectures (27)

Non-classical logic

Non-classical logics (and sometimes alternative logics) are formal systems that differ in a significant way from standard logical systems such as propositional and predicate logic. There are several ways in which this is done, including by way of extensions, deviations, and variations. The aim of these departures is to make it possible to construct different models of logical consequence and logical truth. Philosophical logic is understood to encompass and focus on non-classical logics, although the term has other meanings as well.

Linear logic

Linear logic is a substructural logic proposed by Jean-Yves Girard as a refinement of classical and intuitionistic logic, joining the dualities of the former with many of the constructive properties of the latter. Although the logic has also been studied for its own sake, more broadly, ideas from linear logic have been influential in fields such as programming languages, game semantics, and quantum physics (because linear logic can be seen as the logic of quantum information theory), as well as linguistics, particularly because of its emphasis on resource-boundedness, duality, and interaction.

Logic

Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the science of deductively valid inferences or logical truths. It studies how conclusions follow from premises due to the structure of arguments alone, independent of their topic and content. Informal logic is associated with informal fallacies, critical thinking, and argumentation theory. It examines arguments expressed in natural language while formal logic uses formal language.

CS-101: Advanced information, computation, communication I

Discrete mathematics is a discipline with applications to almost all areas of study. It provides a set of indispensable tools to computer science in particular. This course reviews (familiar) topics a

We introduce Tree-AMP, standing for Tree Approximate Message Passing, a python package for compositional inference in high-dimensional tree-structured models. The package provides a unifying framework to study several approximate message passing algorithms ...

2023

Automatic synthesis of rulesets for programmable stochastic self-assembly of rotationally symmetric robotic modules

Alcherio Martinoli, Bahar Haghighat

Programmable stochastic self-assembly of modular robots provides promising means to formation of structures at different scales. One way to address the design of dedicated control rulesets for self-assembling robotic modules is to leverage formalisms based ...

2017

A Theory Agenda for Component-Based Design

Joseph Sifakis, Simon Bliudze

The aim of the paper is to present a theory agenda for component-based design based on results that motivated the development of the BIP component framework, to identify open problems and discuss further research directions. The focus is on proposing a sem ...

Springer International Publishing2015

Covers the concept of logical equivalence in proofs and inference rules.

Explores the importance of soundness and completeness in a propositional proof system.

Covers the basics of logic, focusing on understanding proofs and constructing valid arguments.