Formalization of metatheory of the Lambda Calculus in constructive type theory using the Barendregt variable convention

Abstarct We formalize in Constructive Type Theory the Lambda Calculus in its classical first-order syntax, employing only one sort of names for both bound and free variables, and with α-conversion based upon name swapping. As a fundamental part of the formalization, we introduce principles of induction and recursion on terms which provide a framework for reproducing the use of the Barendregt Variable Convention as in pen-and-paper proofs within the rigorous formal setting of a proof assistant. The principles in question are all formally derivable from the simple principle of structural induction/recursion on concrete terms. We work out applications to some fundamental meta-theoretical results, such as the Church–Rosser Theorem and Weak Normalization for the Simply Typed Lambda Calculus. The whole development has been machine checked using the system Agda.

I Offend (you) – Parameters of Offense and Verbal Aggression in School

The article examines the manifestations of verbal aggression among students and draws attention to one aspect of it – the insulting words as a component of aggressive human behavior. The study is based on surveys conducted in 19 schools across Bulgaria. A classification of offensive vocabulary has been made. The study registers global trends in modern society, asking questions to psychologists, teachers, sociologists, namely – can aggression be prevented, transformed into a constructive type of behavior, whether the individual could affect the hostile environment etc.

Completeness theorems for first-order logic analysed in constructive type theory

We study various formulations of the completeness of first-order logic phrased in constructive type theory and mechanised in the Coq proof assistant. Specifically, we examine the completeness of variants of classical and intuitionistic natural deduction and sequent calculi with respect to model-theoretic, algebraic, and game-theoretic semantics. As completeness with respect to the standard model-theoretic semantics à la Tarski and Kripke is not readily constructive, we analyse connections of completeness theorems to Markov’s Principle and Weak K̋nig’s Lemma and discuss non-standard semantics admitting assumption-free completeness. We contribute a reusable Coq library for first-order logic containing all results covered in this paper.