# Advances in Proof-Theoretic Semantics

On the Relation Between Heyting's and Gentzen's Approaches to MeaningIntroductionHeyting's Approach to MeaningGentzen's Approach to MeaningA First Comparison Between Heyting's and Gentzen's ApproachesFurther Development of Gentzen's IdeasArgument StructuresArgumentsValidity of ArgumentsWeak and Strong Validity and Their FeaturesMappings of Valid Arguments on BHK-Proofs and Vice VersaExtending the Mapping Proof to Arguments for AExtending the Mapping Arg to BHK-Proofs of AConcluding RemarksReferencesKreisel's Theory of Constructions, the Kreisel-Goodman Paradox, and the Second ClauseIntroductionPredicativity, Decidability, and the BHK InterpretationThe Theory of Constructions and the Second ClauseAn Overview of the Theory of ConstructionsThe Language of TThe Axiomatization of TFormalizing the BHK Interpretation in TSoundness, Completeness, and InternalizationThe Kreisel-Goodman ParadoxThe Reception of the Theory of Constructions and the Second ClauseShifting OpinionsGuilt by Association?Diagnosing the ParadoxSelf-Reference and TypingStratificationDecidabilityReflectionInternalizationConclusions and Further WorkReferencesOn the Paths of CategoriesFunctions of LanguageDeductions Not Necessarily Based on PropositionsDeductions in CategoriesDeductions in Multicategories and PolycategoriesRules for DeductionsReferencesSome Remarks on Proof-Theoretic SemanticsBackground on General Elimination RulesIs Bullet a Logical Constant?The GE-rule for Implication and the Type-Theoretic Dependent Product TypeGE-Rules in GeneralSeveral I-RulesI-Rule Has Several PremissesPremiss of I-Rule Discharges Some AssumptionsGE Harmony: A Counter-ExampleAnother [Counter-]ExampleIn Other WordsConclusionReferencesCategorical Harmony and Paradoxes in Proof-Theoretic SemanticsIntroductionThe Principle of Categorical HarmonyCategorical Harmony in Comparison with Other PrinciplesDegrees of Paradoxicality of Logical ConstantsConcluding Remarks: From Semantic Dualism to DualityReferencesThe Paradox of Knowability from an Intuitionistic StandpointIntroductionAn Intuitionistic Solution(21) is intuitionistically validDefinition 1Truth NotionsInternal and Intuitive TruthUnknown StatementsNeo-Verificationist ApproachesHow Is a Rational Discussion Possible?ConclusionReferencesExplicit Composition and Its Application in Proofs of NormalizationIntroductionNotation for Natural DerivationsStrong Normalization by Bar InductionConcluding Remarks and Further ApplicationsReferencesTowards a Proof-Theoretic Semantics of EqualitiesFrege's QuestionEquality Versus IdentityThe Mode of PresentationMorning Star Versus Evening Star RevisitedEqualityEquality of SensesProof-Theoretic SemanticsReferencesOn the Proof-Theoretic Foundations of Set TheoryIntroductionDefining SetsFunctional Closure, Local Logic and the Notion of AbsolutenessThe Functional ClosureLocal LogicAbsolutenessA Proof-Theoretic InterpretationSetsFoundational IssuesReferencesA Strongly Differing Opinion on Proof-Theoretic Semantics?Tarski's Definition of Logical ConsequenceModel TheoryModel-Theoretic SemanticsDefining Meanings in GeneralDefining Meanings: Specialise Then GeneraliseRepresenting the MeaningDefining Logical ConsequenceReferencesComments on an OpinionOn Dummett's “Proof-Theoretic Justifications of Logical Laws”Analysis of the MethodBoundary RulesSchematic InferencesAssessmentAppendixAuthor's Postscript, January 2015ReferencesSelf-contradictory ReasoningIntroductionMeaning ConditionsThe Liar ParadoxSelf-contradictory Reasoning in N−∀∃=Self-contradictory Reasoning in N−∃=Self-contradictory Reasoning in N−=AppendixNaïve Set TheoryNormal Deductions in a Fragment of NReductions of Deductions in N−=Propositional LogicReferencesCompleteness in Proof-Theoretic SemanticsIntroductionPrawitz's ConjectureFailure of Completeness for Intuitionistic LogicGoldfarb's Account of Dummett's ApproachDefinition 7Proof-Theoretic Validity for Generalized Atomic SystemsGeneralized Atomic SystemsProof-Theoretic ValidityLemma 3Failure of Strong CompletenessStrong Completeness ResultsFailure of CompletenessComparison with Kripke SemanticsA Completeness Result for Intuitionistic LogicDefinition 18Completeness Results for Classical LogicDefinition 19RemarksConclusionReferencesOpen Problems in Proof-Theoretic SemanticsIntroductionThe Nature of Hypotheses and the Format of ProofsOpen Proofs and the Placeholder ViewThe No-Assumptions ViewBidirectionalityLocal and Global Proof-Theoretic SemanticsThe Problem of HarmonyHarmony Based on Generalised RulesHarmony Based on EquivalenceThe Need for an Intensional Notion of HarmonyTowards a Definition of Strong HarmonyProof-Theoretic Semantics Beyond LogicDefinitional ReflectionLogic, Paradoxes, Partial DefinitionsVariables and SubstitutionOutlook: Applications and Extensions of Definitional ReflectionReferences