Concept# Mathematical logic

Summary

Mathematical logic is the study of formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory (also known as computability theory). Research in mathematical logic commonly addresses the mathematical properties of formal systems of logic such as their expressive or deductive power. However, it can also include uses of logic to characterize correct mathematical reasoning or to establish foundations of mathematics.
Since its inception, mathematical logic has both contributed to and been motivated by the study of foundations of mathematics. This study began in the late 19th century with the development of axiomatic frameworks for geometry, arithmetic, and analysis. In the early 20th century it was shaped by David Hilbert's program to prove the consistency of foundational theories. Results of Kurt Gödel, Gerhard Gentzen, and others provided partial resolution to the program, and clarified the issues involved in proving consistency.

Official source

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

Loading

Related people

Loading

Related units

Loading

Related concepts

Loading

Related courses

Loading

Related lectures

Loading

Related publications (64)

Loading

Loading

Loading

Related people (7)

Related units (3)

Related courses (38)

EE-110: Logic systems (for MT)

Ce cours couvre les fondements des systèmes numériques. Sur la base d'algèbre Booléenne et de circuitscombinatoires et séquentiels incluant les machines d'états finis, les methodes d'analyse et de synthèse de systèmelogiques sont étudiées et appliquée

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 as diverse as mathematical reasoning, combinatorics, discrete structures & algorithmic thinking.

COM-500: Statistical signal and data processing through applications

Building up on the basic concepts of sampling, filtering and Fourier transforms, we address stochastic modeling, spectral analysis, estimation and prediction, classification, and adaptive filtering, with an application oriented approach and hands-on numerical exercises.

Related concepts (151)

First-order logic

First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer

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 follo

Mathematics

Mathematics is an area of knowledge that includes the topics of numbers, formulas and related structures, shapes and the spaces in which they are contained, and quantities and their changes. These top

Architectures are common means for organising coordination between components in order to build complex systems and to make them manageable. They allow thinking on a higher plane and avoiding low-level mistakes. Architectures provide means for ensuring correctness-by-construction by enforcing global properties characterising the coordination between components. In this work, we consider the following questions of architecture modelling: 1) how to model architectures; 2) how to compose them if several properties enforced by different architectures are required; 3) how to specify architectures styles that generalise the notion of architectures and represent families of architectures satisfying the same property. An architecture can be considered as an operator that, applied to a set of components, builds a composite component meeting a characteristic property. The underlying concepts of components and their interaction originate from the BIP framework. This thesis is structured in two parts. In the first part, we study the expressiveness of glue operators in the BIP framework. We provide results for classical BIP glue and for several modifications obtained by relaxing the constraints imposed on priority models. We also study an alternative semantics of BIP glue based on the offer predicate. It meets fundamental properties required from component-based frameworks, namely compositionality, incrementality, flattening and modularity. We provide the comparison with the classical BIP semantics and the algorithm for the synthesis of connectors from the interaction logic used to describe coordination constraints. In the second part, we define architectures and propose an architecture composition operator. We study their properties and prove that the composition operator preserves safety properties of its operands. The alternative glue semantics presented in the first part of the thesis allows to extend architectures with priorities. For the specification of architecture styles, we propose configuration logics. We provide a sound and complete axiomatisation of the propositional configuration logic as well as decision procedures for checking that an architecture satisfies a given logical specification. To allow genericity of specifications, we study higher-order extensions of the propositional configuration logic. We illustrate with examples the specification of various architecture styles. We provide an experimental evaluation using the Maude rewriting system to implement the decision procedure for configuration logics. Additionally, we study the relation between the architecture composition operator and the composition of configuration logic formulas.

This research work analyses Theo van Doesburg's Counter-constructions presented in Paris in 1923 at the "L'Effort Moderne" exhibition. These Counter-constructions stand as icons of the Modern Movement due to their role as precursors of a new "boundless" spatiality, a role first intuitively perceived by Le Corbusier or Mies van der Rohe and then theorized by Sigfried Giedion. We have attempted in this research a theoretical study of the Counter-constructions' position within the architectural field. That is to say bringing together their aspect of "spatial manifest" and the Dadaist persona of Theo van Doesburg; this alleged contradiction between the progressive and negative dimension of the Counter-constructions being the subject of this research. It is based on the following problematic: understanding what is at stake in the disjointing of the polychrome plane (as a textile surface) and the suppression of the architectural boundary under the guise of spatial continuity ("the breaking of the enclosure" mentioned by Theo van Doesburg and his interest in the notion of mathematical continuum through the theories of the fourth dimension: Henri Poincaré's Analysis situs). That amounts to studying the modalities connecting the notions of dressing and of continuum to a destructive drive, "throwing out" the inside of the house. The methodology turns towards psychoanalysis through the concepts of Verneinung [negation] (Freud) and Moi-peau [Skin-ego] (Anzieu).

Software systems tend to increase over time in size and complexity. Their development usually spans a long period of time and often results in systems that are hard to understand, debug and maintain. Architectures are common means for organising coordination between components in order to build complex systems and make them manageable. They allow thinking on a higher plane and avoiding low-level mistakes. Grouping architectures that share common characteristics into architecture styles assists component re-use and thus, the cost-effective development of systems. Additionally, architecture styles provide means for ensuring correctness-by-construction by enforcing global properties. The main goal of this thesis is to propose and study formalisms for modelling architectures and architecture styles. For the specification of architectures, we study interaction logics, which are Boolean algebras on a set of component actions. We study a modelling methodology based on first-order interaction logic for writing architecture constraints. To validate the applicability of the approach, we developed the JavaBIP framework that integrates architectures into mainstream software development. JavaBIP receives as input architecture specifications, which it then uses to coordinate software components without requiring access to their source code. JavaBIP implements the principles of the BIP component framework. For the specification of architecture styles, we propose configuration logics, which are powerset extensions of interaction logic. Propositional configuration logic formulas are generated from formulas of interaction logic by using the operators union, intersection and complementation, as well as a coalescing operator. We provide a complete axiomatisation of the propositional configuration logic and a decision procedure for checking that an architecture satisfies given logical specifications. To allow genericity of specifications, we study higher-order extensions of the propositional configuration logic. We provide several examples illustrating the application of configuration logics to the characterisation of architecture styles. For the specification of architecture styles, we also propose architecture diagrams, which is a graphical language rooted in rigorous semantics. We provide methods to assist software developers to specify consistent architecture diagrams, generate the conforming architectures of a style and check whether an architecture model meets given style requirements. We present a full encoding of architecture diagrams into configuration logics. Finally, we report on applications of architecture diagrams to modelling architecture styles identified in realistic case studies of on-board satellite software.

Related lectures (69)