Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Constructive reflection principles for regular theories
Stockholm University, Faculty of Science, Department of Mathematics. University of Oslo.ORCID iD: 0000-0002-5273-8432
Stockholm University, Faculty of Science, Department of Mathematics. (Logik)ORCID iD: 0000-0003-1390-2970
(English)Manuscript (preprint) (Other academic)
Abstract [en]

Classically, any structure for a signature Σ may be completed to a model of a desired regular theory T by means of the chase construction or small object argument. Moreover, this exhibits Mod(T) as weakly reflective in Str(Σ).

We investigate this in the constructive setting. The basic construction is unproblematic, however, it is no longer a weak reflection. Indeed, we show that various reflection principles for models of regular theories are equivalent to choice principles in the ambient set theory. However, the embedding of a structure into its chase-completion still satisfies a conservativity property, which suffices for applications such as the completeness of regular logic with respect to Tarski (i.e. set) models.

Unlike most constructive developments of predicate logic, we do not assume that equality between symbols in the signature is decidable. While in this setting, we also give a version of one classical lemma which is trivial over discrete signatures but more interesting here: the abstraction of constants in a proof to variables.

National Category
Algebra and Logic
Research subject
Mathematical Logic
Identifiers
URN: urn:nbn:se:su:diva-140147OAI: oai:DiVA.org:su-140147DiVA: diva2:1077741
Note

Submitted

Available from: 2017-02-28 Created: 2017-02-28 Last updated: 2017-02-28

Open Access in DiVA

No full text

Other links

arXiv

Search in DiVA

By author/editor
Forssell, HenrikLumsdaine, Peter LeFanu
By organisation
Department of Mathematics
Algebra and Logic

Search outside of DiVA

GoogleGoogle Scholar

Total: 4 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf