Thesis (M. Ed.)--University of Hong Kong, 1996. / Includes bibliographical references (leaf 93-96).

Thesis (M.Ed.)--University of Hong Kong, 1996. / Includes bibliographical references (leaves 93-96). Also available in print.

In contemporary formal theory of truth, model-theoretic and non-classical approaches have been dominant. I rather pursue the so-called classical axiomatic approaches toward truth and my dissertation begins by arguing for the classical axiomatic approach and against the others. The classical axiomatic approach inevitably leads to abandonment of the nave conception of truth and revision of the basic principles of truth derived from that nave conception such as the full T-schema. In the absence of the general guiding principles based on that nave conception, we need to conduct tedious but down-to-earth eld works' of various theories of truth by examining and comparing them from various points of view in searching for satisfactory theories of truth. As such attempt, I raise two new criteria for comparison of truth theories, make a proof-theoretic study of them in connection to the foundation of mathematics.

Made available in DSpace on 2016-04-26T20:20:29Z (GMT). No. of bitstreams: 1 Ester Moreno de Miranda Vieira.pdf: 1218497 bytes, checksum: 4ceadf92303d5c6d54834affcfd1165c (MD5) Previous issue date: 2011-10-18 / This study aims to analyze the theory of evidence that is defined by the logical-semantics constructivism applied to the pension right. Though the several conceptions of the proof word, by a methodological cut, coming from the proof concept as a legal fact in a large sense once established, this legal fact itself in its strict sense has the skills to establish or deconstruct a legal relationship of social security protection through the impact of the law rules. This ability to develop the law effects depends on the legal incidence of the laws, which the logical-semantics Constructivism, opposing to the traditional and worldwide theory of law, does not happen automatically, it depends on the work of a human being, which leads to the promotion of the movement of the standard structures. Analyzed the theory of proof from the perspective of the logical-semantics Constructivism, work combines efforts to demonstrate its applicability under the Social Security Law research field referring to the law protection status. The work inability is identified as the Social Risk and material aspect of such protection standard. Among the specific goals, the leading study seeks to brighten the concept of the "beginning of physical evidence" and analyzes the legitimacy of the so-called taxed evidence according to the General Social Security System / O presente estudo tem por objeto a análise da Teoria das Provas delimitada pelo constructivismo lógico-semântico aplicada ao Direito Previdenciário. Não obstante as diversas concepções do vocábulo prova mediante um corte metodológico, parte-se do conceito de prova como fato jurídico em sentido amplo que, uma vez provado, constitui o fato jurídico em sentido estrito que, por sua vez, tem a aptidão para constituir ou desconstituir a relação jurídica previdenciária de proteção mediante a incidência da norma jurídica. Essa aptidão para desencadear os efeitos jurídicos depende da incidência da norma que, para o Constructivismo Lógico-Semântico, em contraposição à Teoria Geral do Direito Tradicional, não se dá de forma automática, mas antes depende de um ser humano que promova a movimentação das estruturas normativas. Analisada a Teoria da Prova sob a ótica do Constructivismo lógico-semântico, o trabalho reúne esforços para demonstrar sua aplicabilidade no âmbito do Direito Previdenciário no que se refere à relação jurídica de proteção. A incapacidade laboral é identificada como o Risco Social e como aspecto material da norma de proteção. Dentre os objetivos específicos, o presente estudo busca clarificar o conceito de início de prova material e analisar a legalidade das chamadas provas tarifadas em relação ao Regime Geral de Previdência Social

Dependent type theories are a kind of mathematical foundations investigated both for the formalisation of mathematics and for reasoning about programs. They are implemented as the kernel of many proof assistants and programming languages with proofs (Coq, Agda, Idris, Dedukti, Matita, etc). Dependent types allow to encode elegantly and constructively the universal and existential quantifications of higher-order logics and are therefore adapted for writing logical propositions and proofs. However, their usage is not limited to the area of pure logic. Indeed, some recent work has shown that they can also be powerful for driving the construction of programs. Using more precise types not only helps to gain confidence about the program built, but it can also help its construction, giving rise to a new style of programming called Type-Driven Development. However, one difficulty with reasoning and programming with dependent types is that proof obligations arise naturally once programs become even moderately sized. For example, implementing an adder for binary numbers indexed over their natural number equivalents naturally leads to proof obligations for equalities of expressions over natural numbers. The need for these equality proofs comes, in intensional type theories (like CIC and ML) from the fact that in a non-empty context, the propositional equality allows us to prove as equal (with the induction principles) terms that are not judgementally equal, which implies that the typechecker can't always obtain equality proofs by reduction. As far as possible, we would like to solve such proof obligations automatically, and we absolutely need it if we want dependent types to be use more broadly, and perhaps one day to become the standard in functional programming. In this thesis, we show one way to automate these proofs by reflection in the dependently typed programming language Idris. However, the method that we follow is independent from the language being used, and this work could be reproduced in any dependently-typed language. We present an original type-safe reflection mechanism, where reflected terms are indexed by the original Idris expression that they represent, and show how it allows us to easily construct and manipulate proofs. We build a hierarchy of correct-by-construction tactics for proving equivalences in semi-groups, monoids, commutative monoids, groups, commutative groups, semi-rings and rings. We also show how each tactic reuses those from simpler structures, thus avoiding duplication of code and proofs. Finally, and as a conclusion, we discuss the trust we can have in such machine-checked proofs.